Generating tests from counterexamples
Top Cited Papers
- 28 September 2004
- proceedings article
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
We have extended the software model checker BLAST toautomatically generate test suites that guarantee full coveragewith respect to a given predicate. More precisely, givena C program and a target predicate p, BLAST determinesthe set L of program locations which program execution canreach with p true, and automatically generates a set of testvectors that exhibit the truth of p at all locations in L. Wehave used BLAST to generate test suites and to detect deadcode in C programs with up to 30 K lines of code. The analysisand test-vector generation is fully automatic (no userintervention) and exact (no false positives).Keywords
This publication has 17 references indexed in Scilit:
- Abstractions from proofsPublished by Association for Computing Machinery (ACM) ,2004
- Extreme Model CheckingPublished by Springer Nature ,2003
- A system and language for building system-specific, static analysesPublished by Association for Computing Machinery (ACM) ,2002
- Temporal Debugging for Concurrent SystemsPublished by Springer Nature ,2002
- Lazy abstractionPublished by Association for Computing Machinery (ACM) ,2002
- Finding bugs with a constraint solverPublished by Association for Computing Machinery (ACM) ,2000
- Generating test data for branch coveragePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2000
- Automatic test data generation using constraint solving techniquesPublished by Association for Computing Machinery (ACM) ,1998
- Test data generation and feasible path analysisPublished by Association for Computing Machinery (ACM) ,1994
- Symbolic execution and program testingCommunications of the ACM, 1976