@inproceedings{4581,
  abstract     = {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).},
  author       = {Beyer, Dirk and Chlipala, Adam and Henzinger, Thomas A and Jhala, Ranjit and Majumdar, Ritankar},
  booktitle    = {Proceedings of the 26th International Conference on Software Engineering},
  isbn         = {0769521630},
  issn         = {0270-5257},
  location     = {Edinburgh, United Kingdom},
  pages        = {326 -- 335},
  publisher    = {IEEE},
  title        = {{Generating tests from counterexamples}},
  doi          = {10.1109/ICSE.2004.1317455},
  year         = {2004},
}