Journal article

### Making the most of BMC counterexamples

Abstract:

The value of model checking counterexamples for debugging programs (and specifications) is widely recognized. Unfortunately, bounded model checkers often produce counterexamples that are difficult to understand due to the values chosen by a SAT solver. This paper presents two approaches to making better use of BMC counterexamples. The first contribution is a new notion of counterexample minimization that minimizes values with respect to the type system of the language being model checked, rat...

Publication status:
Published
Peer review status:
Peer reviewed
Version:
Publisher's Version

### Access Document

Files:
• (pdf, 280.2kb)
Publisher copy:
10.1016/j.entcs.2004.12.023

### Authors

More by this author
Department:
Oxford, MPLS, Computer Science
Publisher:
Elsevier Publisher's website
Journal:
Electronic Notes in Theoretical Computer Science Journal website
Volume:
119
Issue:
2
Pages:
67-81
Publication date:
2005-03-01
DOI:
ISSN:
1571-0661
Pubs id:
pubs:327189
URN:
uri:294519b5-f4a5-43b5-b55b-8b0d3e0f744e
UUID:
uuid:294519b5-f4a5-43b5-b55b-8b0d3e0f744e
Local pid:
pubs:327189
Keywords:

### Metrics

If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP