Whodunit? Causal analysis for counterexamples

Chao Wang, Zijiang Yang, Franjo Ivančić, Aarti Gupta

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

31 Scopus citations


Although the counterexample returned by a model checker can help in reproducing the symptom related to a defect, a significant amount of effort is often required for the programmer to interpret it in order to locate the cause. In this paper, we provide an automated procedure to zoom in to potential software defects by analyzing a single concrete counterexample. Our analysis relies on extracting from the counterexample a syntactic-level proof of infeasibility, i.e., a minimal set of word-level predicates that contradict with each other. The procedure uses an efficient weakest pre-condition algorithm carried out on a single concrete execution path, which is significantly more scalable than other model checking based approaches. Unlike most of the existing methods, we do not need additional execution traces other than the buggy one. We use public-domain examples to demonstrate the effectiveness of our new algorithm.

Original languageEnglish (US)
Title of host publicationAutomated Technology for Verification and Analysis - 4th International Symposium, ATVA 2006, Proceedings
PublisherSpringer Verlag
Number of pages14
ISBN (Print)3540472371, 9783540472377
StatePublished - 2006
Event4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006 - Beijing, China
Duration: Oct 23 2006Oct 26 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4218 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Whodunit? Causal analysis for counterexamples'. Together they form a unique fingerprint.

Cite this