Abstraction-driven concolic testing Conference Paper

Author(s): Daca, Przemysław; Gupta, Ashutosh K; Henzinger, Thomas A
Title: Abstraction-driven concolic testing
Title Series: LNCS
Affiliation IST Austria
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 concolictesting 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.
Keywords: Search spaces; Branch coverage; Concolic testing; Counterexample-guided abstraction refinement; Coverage criteria; Large programs; Model checker; Path explosions
Conference Title: VMCAI: Verification, Model Checking and Abstract Interpretation
Volume: 9583
Conference Dates: January 17 - 19, 2016
Conference Location: St. Petersburg, FL, USA
Publisher: Springer  
Date Published: 2016-01-01
Start Page: 328
End Page: 347
DOI: 10.1007/978-3-662-49122-5_16
Notes: We thank Andrey Kupriyanov for feedback on the manuscript, and Michael Tautschnig for help with preparing the experiments. This research was supported in part by the European Research Council (ERC) under grant 267989 (QUAREM) and by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award).
Open access: yes (repository)
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
  2. Ashutosh Gupta
    16 Gupta
  3. Przemysław, Daca
    12 Daca
Related IST Austria Work