First-Order and Second-Order Symbolic Execution
Symbolic execution is a program analysis technique relying on satisfiability modulo theories, in which the program is executed with symbolic variables instead of concrete values, and the result of such execution is a set of formulas over the symbolic variables. Symbolic execution has found many applications including bugs/vulnerability finding, test generation, verification, etc. The first part of this talk introduces main challenges of traditional first-order symbolic execution, and discusses some algorithmic and engineering approaches to address these challenges. The second part of the talk presents an extension of symbolic execution for second-order logic, that can be used to solve more complex problems such as automated program repair and environment modelling.
- Cristian Cadar, Daniel Dunbar, Dawson Engler. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs // OSDI 2008
- Edward J. Schwartz, Thanassis Avgerinos, David Brumley. All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask) // S&P 2010
- Sergey Mechtaev, Alberto Griggio, Alessandro Cimatti, Abhik Roychoudhury. Symbolic Execution with Existential Second-Order Constraints // FSE 2018
Presenter: Sergey Mechtaev, University College of London