Optimizing constraint solving in second-order symbolic execution

Research-oriented individual project
Keywords: satisfiability modulo theories, symbolic execution, program synthesis

Symbolic execution is a powerful program analysis technique whose main idea is to to use symbolic values, instead of concrete values, as inputs, and to represent the values of program variables as symbolic expressions over the symbolic values. Symbolic execution has found many applications such as test generation, bug and vulnerability detection, formal verification, debugging, etc. Symbolic execution with existential second order constraints (SE-ESOC) is a recently proposed extension of symbolic execution that allows to introduce second-order symbolic variables that range over functions rather than values. For example, given a function search(pred, data) that searches for an element of the array data that satisfies the predicate pred, it allows to answer such questions as "what predicate would make search return 2, given the array [0, 1, 2]?". This functionality opens a lot of new opportunities such as automatically correcting software bugs, synthesizing execution environment models, testing functional programs, etc. However, one of the major limitations of SE-ESOC is that it has to solve complex second-order logical constraints that reduces its efficiency. The goal of this project is to optimise second-order constraint solving in SE-ESOC.

Goals

Required skills

Relevant links & publications