Whodunit? Causal Analysis for Counterexamples

12 years 5 months ago
Whodunit? Causal Analysis for Counterexamples
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.
Chao Wang, Zijiang Yang, Franjo Ivancic, Aarti Gup
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where ATVA
Authors Chao Wang, Zijiang Yang, Franjo Ivancic, Aarti Gupta
Comments (0)