Evaluating the Effectiveness of an OOX based Symbolic Execution Engine
MetadataShow full item record
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.
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 veriﬁcation of software. A notorious problem with formal veriﬁcation is the path explosion problem: the exponentially increasing requirement of computing power to verify ...
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 ...
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 ...