Making the most of BMC counterexamples
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 be...
| Main Authors: | , |
|---|---|
| Format: | Journal article |
| Published: |
Elsevier
2005
|
| _version_ | 1797059641122750464 |
|---|---|
| author | Groce, A Kroening, D |
| author_facet | Groce, A Kroening, D |
| author_sort | Groce, A |
| collection | OXFORD |
| description | 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, rather than at the level of SAT variables. Greedy and optimal approaches to the minimization problem are presented and compared. The second contribution extends a BMC-based error explanation approach to automatically hypothesize causes for the error in a counterexample. These hypotheses (in terms of relationships between variables) can be automatically checked to determine if a causal dependence exists. Experimental results show that causes can be automatically determined for errors in interesting ANSI C programs. © 2005 Elsevier B.V. |
| first_indexed | 2024-03-06T20:07:09Z |
| format | Journal article |
| id | oxford-uuid:294519b5-f4a5-43b5-b55b-8b0d3e0f744e |
| institution | University of Oxford |
| last_indexed | 2024-03-06T20:07:09Z |
| publishDate | 2005 |
| publisher | Elsevier |
| record_format | dspace |
| spelling | oxford-uuid:294519b5-f4a5-43b5-b55b-8b0d3e0f744e2022-03-26T12:18:12ZMaking the most of BMC counterexamplesJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:294519b5-f4a5-43b5-b55b-8b0d3e0f744eSymplectic Elements at OxfordElsevier2005Groce, AKroening, DThe 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, rather than at the level of SAT variables. Greedy and optimal approaches to the minimization problem are presented and compared. The second contribution extends a BMC-based error explanation approach to automatically hypothesize causes for the error in a counterexample. These hypotheses (in terms of relationships between variables) can be automatically checked to determine if a causal dependence exists. Experimental results show that causes can be automatically determined for errors in interesting ANSI C programs. © 2005 Elsevier B.V. |
| spellingShingle | Groce, A Kroening, D Making the most of BMC counterexamples |
| title | Making the most of BMC counterexamples |
| title_full | Making the most of BMC counterexamples |
| title_fullStr | Making the most of BMC counterexamples |
| title_full_unstemmed | Making the most of BMC counterexamples |
| title_short | Making the most of BMC counterexamples |
| title_sort | making the most of bmc counterexamples |
| work_keys_str_mv | AT grocea makingthemostofbmccounterexamples AT kroeningd makingthemostofbmccounterexamples |