Journal article icon

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

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

Actions


Access Document


Files:
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:

Terms of use


Metrics



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

TO TOP