Generating Tests From Counterexamples

The authors 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. They 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).