Deterministic state space exploration

Abstract Symbolic execution is a very active research area due to its automatic test-case generation, bug finding, and many more applications. Despite the many recent proposals for improvements, we find it hard to quantify how state-of-the-art progresses. One reason is the variety of programming languages, features, and symbolic execution engines to support them. Still, even if we compare a single symbolic execution engine (A) and the same engine with some modifications (A*) and run the implementations with the same benchmarks, reasoning about the actual cause of the differences between them is complex. While artefacts (here benchmarks, measurements, data, and implementation) provide an invaluable base for reproducible research, the implementation itself is often treated as a black box. Changes in behaviour between two implementations are quantified based on the coarse-grain difference in benchmark behaviour, i.e. changed code coverage or execution time. We propose a complementing fine-grain approach that helps to understand implementations far better — not only supporting reproducible research, but also supporting the development of the implementation in the first place. In this paper, we analyse KLEE, a well-established symbolic execution engine for C and C++, and identify significant challenges that make evaluating and comparing different implementations hard. We identify implementation-specific reasons for KLEE that can often be transferred to other symbolic execution engines and present ways to fix them. We propose Deterministic State-Space Exploration as one technique that helps to quantify and validate incremental improvements of symbolic execution engines.