loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
26th International Conference on Software Engineering (ICSE'04)
Generating Tests from Counterexamples
Edinburgh, Scotland, United Kingdom
May 23-May 28
ISBN: 0-7695-2163-0
ASCII Text
x 
 
Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, "Generating Tests from Counterexamples," Software Engineering, International Conference on, pp. 326-335, 26th International Conference on Software Engineering (ICSE'04), 2004.
 
 
BibTex
x
 
@article{ 10.1109/ICSE.2004.1317455,
author = {Dirk Beyer and Adam J. Chlipala and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar},
title = {Generating Tests from Counterexamples},
journal ={Software Engineering, International Conference on},
volume = {0},
year = {2004},
issn = {0270-5257},
pages = {326-335},
doi = {http://doi.ieeecomputersociety.org/10.1109/ICSE.2004.1317455},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Software Engineering, International Conference on
TI - Generating Tests from Counterexamples
SN - 0270-5257
SP326
EP335
A1 - Dirk Beyer,
A1 - Adam J. Chlipala,
A1 - Thomas A. Henzinger,
A1 - Ranjit Jhala,
A1 - Rupak Majumdar,
PY - 2004
KW - null
VL - 0
JA - Software Engineering, International Conference on
ER -
 
Dirk Beyer, University of California at Berkeley
Adam J. Chlipala, University of California at Berkeley
Thomas A. Henzinger, University of California at Berkeley
Ranjit Jhala, University of California, Berkeley
Rupak Majumdar, University of California at Los Angeles
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).
Citation:
Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, "Generating Tests from Counterexamples," icse, pp.326-335, 26th International Conference on Software Engineering (ICSE'04), 2004
Usage of this product signifies your acceptance of the Terms of Use.