TY - JOUR
T1 - Making the most of BMC counterexamples
AU - Groce, Alex
AU - Kroening, Daniel
N1 - Funding Information:
1 This research was sponsored by the Gigascale Systems Research Center (GSRC) under contract no. 9278-1-1010315, the National Science Foundation (NSF) under grant no. CCR-9803774, the Office of Naval Research (ONR), the Naval Research Laboratory (NRL) under contract no. N00014-01-1-0796, the Army Research Office (ARO) under contract no. DAAD19-01-1-0485, and the General Motors Collaborative Research Lab at CMU. The views and conclusions contained in this document are those of the author and should not be interpreted as representing the official policies, either expressed or implied, of GSRC, NSF, ONR, NRL, ARO, GM, or the U.S. government. 2 Email: [email protected] 3 Email: [email protected]
PY - 2005/3/14
Y1 - 2005/3/14
N2 - 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.
AB - 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.
KW - Counterexamples
KW - Error explanation
KW - Model checking
UR - http://www.scopus.com/inward/record.url?scp=14644392232&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=14644392232&partnerID=8YFLogxK
U2 - 10.1016/j.entcs.2004.12.023
DO - 10.1016/j.entcs.2004.12.023
M3 - Conference article
AN - SCOPUS:14644392232
SN - 1571-0661
VL - 119
SP - 67
EP - 81
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
IS - 2
T2 - Proceedings of the 2nd International Workshop on Bounded Model Checking (BMC 2004).
Y2 - 18 July 2004 through 18 July 2004
ER -