Abstraction-driven Concolic Testing

TL;DR

This paper introduces a hybrid approach combining concolic testing and model checking to improve code coverage in large programs, effectively addressing path explosion and scalability issues.

Contribution

It presents a novel iterative method that refines program abstraction to enhance concolic testing efficiency, implemented on CREST and CpaChecker tools.

Findings

Improved branch coverage from 48% to 63% in best cases.

Achieved average coverage increase from 66% to 71%.

Demonstrated effectiveness on SvComp benchmarks.

Abstract

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 abstraction 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 CpaChecker. We evaluated our tool on a collection of programs and a category of SvComp benchmarks. In our experiments, we observed an improvement in branch coverage compared to CREST from 48% to 63% in the best case, and from 66% to 71% on average.