ion-driven Concolic Testing‹ Przemyslaw Daca1 , Ashutosh Gupta2 , and Thomas A. Henzinger1 1 IST Austria, Austria 2 Tata Institute for Fundamental Research, India Concolic testing is a promising method for generating test suites for large programs. However, it suffers from the path-explosion problem and often fails to find tests that cover difficult-to-reach parts of programs. In contrast, model checkers based on counterexample-guided ion refinement explore programs exhaustively, while failing to scale on large programs with precision. In this paper, we present a novel method that iteratively combines concolic testing and model checking to find a test suite for a given coverage criterion. If concolic testing fails to cover some test goals, then the model checker refines its program abstraction to prove more paths infeasible, which reduces the search space for concolic testing. We have implemented our method on top of the concolic-testing tool Crest and the model checker CpaCheck...
Przemyslaw Daca, Ashutosh Gupta, Thomas A. Henzing