Fitness-Guided Path Exploration in Dynamic Symbolic Execution

Dynamic symbolic execution is a structural testing technique that systematically explores feasible paths of the program under test by running the program with different test inputs. Its main goal is to find a set of test inputs that lead to the coverage of particular test targets, e.g., specific state- ments or violated assertions. In theory, it is undecidable whether a test target can be covered, and in practice the number of feasible paths explodes. Nevertheless, for many programs, heuristic search strategies can often cover a test target quickly by analyzing only a few potentially feasible paths. We propose a novel approach called Fitnex, a search strategy that uses state-dependent fitness values (computed through a fitness function) to guide path exploration. The fitness function measures how close an already discovered feasible path is to a particular test target. Our new search strategy gives paths with better fitness values higher priority in the search. As a result, the search needs to consider fewer paths to cover test targets faster. Our new fitness-guided search strategy can be integrated with other strategies that are effective for exploration problems where the fitness heuristic fails. We implemented the new approach in Pex, an automated structural testing tool developed at Microsoft Research for .NET programs. We evaluated the new approach on a set of micro-benchmark programs. The results show that the new approach is effective since it consistently achieves high code coverage faster than existing search strategies.