Abstraction-driven concolic testing

DOI10.1007/978-3-662-49122-5_16MaRDI QIDQ2796059zbMATH OpenOpenAlexFDO

Authors Przemysław Daca, Ashutosh Gupta, Thomas A. Henzinger

Publication date 23 March 2016

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1511.02615

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

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.

Recommendations

• Query-Driven Program Testing
• On the completeness of selective unification in concolic testing of logic programs
• Concolic testing in CLP
• Concolic testing in logic programming
• Sound and complete concolic testing for higher-order functions

Cited in

(10)

• Reusing predicate precision in value analysis
• Sound and complete concolic testing for higher-order functions
• On the completeness of selective unification in concolic testing of logic programs
• Test-design through abstraction: A systematic approach based on the refinement calculus
• Query-Driven Program Testing
• Information Exchange Between Over- and Underapproximating Software Analyses
• Symbolic encoding of LL(1) parsing and its applications
• Parallel program analysis via range splitting
• Towards efficient data-flow test data generation
• Concolic testing heap-manipulating programs

This page was built for publication: Abstraction-driven concolic testing

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2796059)