Generating tests from counterexamples

Author

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

Author_Institution

Electr. Eng. & Comput. Sci., Univ. of California, Berkeley, CA, USA

fYear

2004

fDate

23-28 May 2004

Firstpage

326

Lastpage

335

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

Keywords

C language; automatic programming; program testing; program verification; BLAST; C program; counterexamples; program execution; program locations; software model checker; target predicate; test generation; test suite generation; test vector generation; Automata; Automatic testing; Computer science; Computerized monitoring; Concrete; Condition monitoring; Linux; Safety; Security; Software testing;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Engineering, 2004. ICSE 2004. Proceedings. 26th International Conference on

ISSN

0270-5257

Print_ISBN

0-7695-2163-0

Type

conf

DOI

10.1109/ICSE.2004.1317455

Filename

1317455