TY - CONF AB - 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 p, BLAST determines the set L of program locations which program execution can reach with p true, and automatically generates a set of test vectors that exhibit the truth of p at all locations in L. 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). AU - Beyer, Dirk AU - Chlipala, Adam J AU - Thomas Henzinger AU - Jhala, Ranjit AU - Majumdar, Ritankar S ID - 4581 TI - Generating tests from counterexamples ER -