Title
Automatic Test Generation for Coverage Analysis Using CBMC
Abstract
Testing is the most used technique for software verification: it is easy to use and even if no error is found, it can release a set of tests certifying the (partial) correctness of the compiled system. Moreover, in order to increase the confidence of the correctness of the compiled system, it is often required that the provided set of tests covers 100% of the code. This requirement, however, substantially increases the costs associated to the testing phase, since it may involve the manual generation of tests. In this paper we show how to use a Bounded Model Checker for C programs (CBMC) as an automatic test generator for the Coverage Analysis, and we show how its use can substantially reduce the costs of the testing phase.
Year
DOI
Venue
2009
10.1007/978-3-642-04772-5_38
EUROCAST
Keywords
Field
DocType
automatic test generator,software verification,manual generation,automatic test generation,coverage analysis,c program,bounded model checker,used technique,testing phase
Model checking,Fault coverage,Computer science,Correctness,Algorithm,Theoretical computer science,Dynamic testing,Conjunctive normal form,Symbolic execution,Modified condition/decision coverage,Reliability engineering,Software verification
Conference
Volume
ISSN
Citations 
5717
0302-9743
4
PageRank 
References 
Authors
0.50
12
5
Name
Order
Citations
PageRank
Damiano Angeletti1333.49
Enrico Giunchiglia22380164.28
Massimo Narizzano345130.41
Alessandra Puddu4232.31
Salvatore Sabina5253.45