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 ... -
Learning board game rules by observing game play, a comparison of symbolic and non-symbolic AI
Teekens, S.V. (2020)Usually the focus of Artificial Intelligence (AI) game research is on learning strategies for specific games. This thesis reversed this focus by looking for methods capable of learning game rules in general. The goal is ... -
The role of PcG and TrxG proteins in executing epigenetic memory
Bodor, D. (2010)Cells with identical genomes can have very different identities and functions. This variability is in part controlled by epigenetic mechanisms that regulate differential gene expression, stabilize genetic programs throughout ...