kirancodes.me
To Proof Maintenance & Beyond!
ICSE 2004

Generating Tests from Counterexamples

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

DOI 10.1109/icse.2004.1317455dblp

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).

BibTeX
@inproceedings{Beyer-al:ICSE04,
  author    = {Dirk Beyer and
               Adam Chlipala and
               Thomas A. Henzinger and
               Ranjit Jhala and
               Rupak Majumdar},
  title     = {Generating Tests from Counterexamples},
  booktitle = {ICSE},
  pages     = {326--335},
  publisher = {{IEEE} Computer Society},
  year      = {2004},
}

Related papers