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.