@inproceedings{2a045c580f4943e7b93a51295b27ce4b,
title = "Whodunit? Causal analysis for counterexamples",
abstract = "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.",
author = "Chao Wang and Zijiang Yang and Franjo Ivan{\v c}i{\'c} and Aarti Gupta",
year = "2006",
doi = "10.1007/11901914_9",
language = "English (US)",
isbn = "3540472371",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "82--95",
booktitle = "Automated Technology for Verification and Analysis - 4th International Symposium, ATVA 2006, Proceedings",
address = "Germany",
note = "4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006 ; Conference date: 23-10-2006 Through 26-10-2006",
}