First-Order and Second-Order Symbolic Execution

1 April 2019

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.

Supplementary materials:

  1. Cristian Cadar, Daniel Dunbar, Dawson Engler. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs // OSDI 2008
  2. 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
  3. Sergey Mechtaev, Alberto Griggio, Alessandro Cimatti, Abhik Roychoudhury. Symbolic Execution with Existential Second-Order Constraints // FSE 2018

Presenter: Sergey Mechtaev, University College of London