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.