Explaining abstract counterexamples

Sagar Chaki, Alex Groce, Ofer Strichman

Research output: Contribution to conferencePaperpeer-review

50 Scopus citations


When a program violates its specification a model checker produces a counterexample that shows an example of undesirable behavior. It is up to the user to understand the error, locate it, and fix the problem. Previous work introduced a technique for explaining and localizing errors based on finding the closest execution to a counterexample, with respect to a distance metric. That approach was applied only to concrete executions of programs. This paper extends and generalizes the approach by combining it with predicate abstraction. Using an abstract state-space increases scalability and makes explanations more informative. Differences between executions are presented in terms of predicates derived from the specification and program, rather than specific changes to variable values. Reasoning to the cause of an error from the fact that in the failing run x < y, but in the successful execution x = y is easier than reasoning from the information that in the failing run y = 239, but in the successful execution y = 232. An abstract explanation is automatically generalized. Predicate abstraction has previously been used in model checking purely as a state-space reduction technique. However, an abstraction good enough to enable a model checking tool to find an error is also likely to be useful as an automatically generated high-level description of a state space -suitable for use by programmers. Results demonstrating the effectiveness of abstract explanations support this claim.

Original languageEnglish (US)
Number of pages10
StatePublished - 2004
Externally publishedYes
EventTwelfth ACM SIGSOFT International Symposium on the Foundations of Software Engineering, SIGSOFT 2004/FSE-12 - Newport Beach, CA, United States
Duration: Oct 31 2004Nov 5 2004


ConferenceTwelfth ACM SIGSOFT International Symposium on the Foundations of Software Engineering, SIGSOFT 2004/FSE-12
Country/TerritoryUnited States
CityNewport Beach, CA


  • Fault localization
  • Model checking
  • Predicate abstraction

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Explaining abstract counterexamples'. Together they form a unique fingerprint.

Cite this