Solving constraints for generational search

Abstract

Concolic testing is an automated software testing method that combines concrete and symbolic execution to achieve high code coverage and expose bugs in the program under test. During an execution of the program, constraints over the input variables are collected. Then, by changing these constraints in a systematic manner and solving the thereby derived constraint systems, new inputs can be obtained that force the program to execute along yet undiscovered program paths. The performance of the constraint solving step is crucial for the scalability of such an approach. In this paper, we are specifically concerned with solving the constraint systems obtained when employing the concolic testing search strategy known as Generational Search. We implemented several methods for preprocessing and solving the systems using the SMT solvers MathSAT, STP, Yices, and Z3, and evaluated the methods and solvers on constraints generated by the concolic execution engine Crest. © 2013 Springer-Verlag.