Explaining Counterexamples Using Causality

Ilan Beer*, Shoham Ben-David, Hana Chockler, Avigail Orni, Richard Trefler

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference paper

54 Citations (Scopus)

Abstract

When a model does not satisfy a given specification, a counterexample is produced by the model checker to demonstrate the failure. A user must then examine the counterexample trace, in order to visually identify the failure that it demonstrates. If the trace is long, or the specification is complex, finding the failure in the trace becomes a non-trivial task. In this paper, we address the problem of analyzing a counterexample trace and highlighting the failure that it demonstrates. Using the notion of causality, introduced by Halpern and Pearl, we formally define a set of causes for the failure of the specification on the given counterexample trace. These causes are marked as red dots and presented to the user as a visual explanation of the failure. We study the complexity of computing the exact set of causes, and provide a polynomial-time algorithm that approximates it. This algorithm is implemented as a feature in the IBM formal verification platform RuleBase PE, where these visual explanations are an integral part of every counterexample trace. Our approach is independent of the tool that produced the counterexample, and can be applied as a light-weight external layer to any model checking tool, or used to explain simulation traces.

Original languageEnglish
Title of host publicationComputer aided verification
Subtitle of host publication21st international conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009 ; proceedings
EditorsA Bouajjani, O Maler
Place of PublicationBerlin
PublisherSpringer-Verlag Berlin Heidelberg
Pages94-108
Number of pages15
VolumeN/A
EditionN/A
ISBN (Print)9783642026577
Publication statusPublished - 2009
Event21st International Conference on Computer Aided Verification - Grenoble, France
Duration: 26 Jun 20092 Jul 2009

Publication series

NameLecture Notes in Computer Science
PublisherSPRINGER-VERLAG BERLIN
Volume5643
ISSN (Print)0302-9743

Conference

Conference21st International Conference on Computer Aided Verification
Country/TerritoryFrance
CityGrenoble
Period26/06/20092/07/2009

Keywords

  • TEMPORAL LOGIC
  • MODEL CHECKING

Fingerprint

Dive into the research topics of 'Explaining Counterexamples Using Causality'. Together they form a unique fingerprint.

Cite this