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).

• Type: Conference
• Year: 2004
• Where: ICSE
• Authors: Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
• Keywords: ICSE 2004, Model Checker Blast, Software Engineering, Target Predicate, Test Suites