Generating Tests from Counterexamples

9 years 10 months ago
Generating Tests from Counterexamples
We have extended the software model checker BLAST to automatically generate test suites that guarantee full coverage with respect to a given predicate. More precisely, given a C program and a target predicate ?, BLAST determines the set ? of program locations which program execution can reach with ? true, and automatically generates a set of test vectors that exhibit the truth of ? at all locations in ?. We have used BLAST to generate test suites and to detect dead code in C programs with up to 30 K lines of code. The analysis and test-vector generation is fully automatic (no user intervention) and exact (no false positives).
Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger,
Added 09 Dec 2009
Updated 09 Dec 2009
Type Conference
Year 2004
Where ICSE
Authors Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
Comments (0)