Making the most of BMC counterexamples

Alex Groce, Daniel Kroening

Research output: Contribution to journalConference articlepeer-review

29 Scopus citations


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.

Original languageEnglish (US)
Pages (from-to)67-81
Number of pages15
JournalElectronic Notes in Theoretical Computer Science
Issue number2
StatePublished - Mar 14 2005
Externally publishedYes
EventProceedings of the 2nd International Workshop on Bounded Model Checking (BMC 2004). -
Duration: Jul 18 2004Jul 18 2004


  • Counterexamples
  • Error explanation
  • Model checking

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Making the most of BMC counterexamples'. Together they form a unique fingerprint.

Cite this