The Path Explosion Problem in Symbolic Execution: An Approach to the Effects of Concurrency and Aliasing

Abstract

Symbolic Execution is a technique used for the formal verification of software. A notorious problem with formal verification is the path explosion problem: the exponentially increasing requirement of computing power to verify more complex software. Common contributors to the path explosion problem are: (1) loops and recursion; (2) exceptions; (3) pointer aliasing; and (4) concurrency. In this thesis, we present an intermediate verification language: the OOX language. OOX is intended as a core language for object-oriented languages with support for concurrency, such as Java and C#. We developed a symbolic execution engine for OOX, which aims to limit the effects of the path explosion problem resulting from the first, third and fourth contributors. To achieve this, we applied three main optimizations: partial order reduction, formula caching and expression evaluation. Furthermore, the logic to handle references is defined in the front-end of our approach. We use a SMT solver as a back-end to give a definitive answer when the front-end does not give a definitive answer. The results of this approach show a positive image. The optimizations drastically reduce the runtime and our approach can compete with existing tools like CBMC and CIVL.