TY - GEN
T1 - Whodunit? Causal analysis for counterexamples
AU - Wang, Chao
AU - Yang, Zijiang
AU - Ivančić, Franjo
AU - Gupta, Aarti
N1 - Copyright:
Copyright 2020 Elsevier B.V., All rights reserved.
PY - 2006
Y1 - 2006
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=33845216260&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=33845216260&partnerID=8YFLogxK
U2 - 10.1007/11901914_9
DO - 10.1007/11901914_9
M3 - Conference contribution
AN - SCOPUS:33845216260
SN - 3540472371
SN - 9783540472377
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 82
EP - 95
BT - Automated Technology for Verification and Analysis - 4th International Symposium, ATVA 2006, Proceedings
PB - Springer Verlag
T2 - 4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006
Y2 - 23 October 2006 through 26 October 2006
ER -