Evaluating the Effectiveness of an OOX based Symbolic Execution Engine

Abstract

Symbolic execution is a program testing technique from the software verification domain. It involves symbolically modeling and testing all possible execution paths of a program against a set of constraints. The three main challenges of symbolic execution are (1) Memory modeling; (2) Execution path explosion; and (3) Constraint solving.

In this thesis, we present a Symbolic Execution Engine. This engine operates on the OOX language and is equipped with eleven different heuristics. These heuristics aim to improve efficiency in handling the second and third challenges of symbolic execution.

We conducted an extensive experiment with our Symbolic Execution Engine. We used the benchmarking tools and a set of 81 benchmarking programs from the Software Verification Competition, and seven comparable verification tools, with the aim of investigating the effectiveness of the heuristics and substantiating the claims of effectiveness, soundness, and completeness of our Symbolic Execution Engine.