Generating Tests from Counterexamples

Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar

We extend the software model checker BLAST to automatically generate test suites that guarantee full coverage with respect to a given predicate, or with respect to a more general temporal safety property. More precisely, given a C program and a predicate p, extended BLAST determines the set L of program locations in which the predicate can be true, and automatically generates a set of test cases that exhibit the truth of p at all locations in L. We have used extended BLAST to generate test suites for security disciplines, and o detect dead code, in C programs with up to 30K lines of code. The analysis and test-case generation is fully automatic (no user intervention) and exact (no false positives).

Proceedings of the 26th ACM/IEEE International Conference on Software Engineering (ICSE), IEEE Computer Society Press, 2004.

PostScript PDF © 2003.