Test Case Selection Based on Path Condtions of Symbolic Execution

Symbolic execution as a test case generation technique has recently become an active research area. However, since symbolic execution generates a large number of test cases, it is impractical to run all the generated test cases in practice. In this paper, we present a test case selection method for a symbolic execution-based test case generation. This method has the following two characteristics. 1)Test cases which cover atomic conditions collected during symbolic execution, called path condition-based, are selected to keep the fault-detection capability. 2)This method does not depend on a particular symbolic execution engine since it is based on an analysis of path conditions in a general format. We implemented this method in our tool and evaluated this method with real systems. Our evaluation shows that the method produces a significant reduction in the size of the test suite while effectively preserving its fault-detection capability. We also demonstrate that the method is compatible with practically any symbolic execution engine, including the popular tools Java Path Finder and KLEE.