Concolic Walk Heuristic
The Concolic Walk algorithm is a heuristic for solving complicated arithmetic path conditions.
Test input generators using symbolic and concolic execution must solve path conditions to systematically explore a program and generate high coverage tests. However, programs may contain complicated arithmetic path conditions, which are undecidable in general; and constraint solvers usually cannot handle calls to native library methods. Our algorithm combines linear constraint solving and heuristic search to overcome these limitations. On a corpus of 11 programs, the Concolic Walk algorithm generates tests with two- to three-times higher coverage than simplification-based tools such as jCUTE, while being up to five-times as efficient. Furthermore, it improves the coverage of two state-of-the-art test generators by 21% and 32%. Other concolic and symbolic testing tools could integrate our algorithm to solve complex path conditions without having to sacrifice any of their own capabilities, leading to higher overall coverage.
Our implementation of the Concolic Walk (CW) algorithm is an extension of Symbolic PathFinder (SPF), which is a symbolic execution engine built on top of the Java PathFinder (JPF) verification framework. The extension works with existing SPF test-drivers; the only change required is setting a configuration flag to enable the extension.
- Peter Dinges and Gul Agha. Solving Complex Path Conditions through Heuristic Search on Induced Polytopes. In Shing-Chi Cheung, Alessandro Orso, and Margaret-Anne Storey, editors, FSE 2014 - 22nd ACM SIGSOFT International Symposium on the Foundations of Software Engineering, November 15-19, Hong Kong, 2014.
See the project's Github page for the source code of the modified version of Symbolic PathFinder that implements the heuristic. The repository also contains documentation, the scripts for running experiments, and the data collected during the evaluation of the heuristic.
The implementation of the Concolic Walk algorithm and its unit tests, the BruteFuzz tool, and the evaluation scripts are available under the MIT license. Copyright (c) 2014 the University of Illinois Board of Trustees. All Rights Reserved.
This work was supported in part by sponsorship from the Army Research Office under award number W911NF-09-1-0273, as well as the Air Force Research Laboratory and the Air Force Office of Scientific Research under agreement number FA8750-11-2-0084.
Please contact Peter Dinges if you have questions, remarks, or suggestions regarding the project.