Evaluating the Effectiveness of an OOX based Symbolic Execution Engine
Summary
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.
Collections
Related items
Showing items related by title, author, creator and subject.
-
The Path Explosion Problem in Symbolic Execution: An Approach to the Effects of Concurrency and Aliasing
Koppier, S. (2020)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 ... -
Partial Order Reduction in Symbolic Execution for Object-Oriented Languages
Vrooman, Jesse (2024)The path explosion problem is a significant issue for verification tools that use symbolic execution. Monotonic partial order reduction introduces a sound and complete method of pruning paths irrelevant to the verification ...