Whodunit? Causal analysis for counterexamples

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

doi:10.1007/11901914_9

Whodunit? Causal analysis for counterexamples

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

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

18 Scopus citations

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.

Original language	English (US)
Title of host publication	Automated Technology for Verification and Analysis - 4th International Symposium, ATVA 2006, Proceedings
Publisher	Springer Verlag
Pages	82-95
Number of pages	14
ISBN (Print)	3540472371, 9783540472377
DOIs	https://doi.org/10.1007/11901914_9
State	Published - 2006
Event	4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006 - Beijing, China Duration: Oct 23 2006 → Oct 26 2006

Publication series

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

Other

Other	4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006
Country	China
City	Beijing
Period	10/23/06 → 10/26/06

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/11901914_9

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

Cite this

Wang, C., Yang, Z., Ivančić, F., & Gupta, A. (2006). Whodunit? Causal analysis for counterexamples. In Automated Technology for Verification and Analysis - 4th International Symposium, ATVA 2006, Proceedings (pp. 82-95). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4218 LNCS). Springer Verlag. https://doi.org/10.1007/11901914_9

Wang, Chao ; Yang, Zijiang ; Ivančić, Franjo ; Gupta, Aarti. / Whodunit? Causal analysis for counterexamples. Automated Technology for Verification and Analysis - 4th International Symposium, ATVA 2006, Proceedings. Springer Verlag, 2006. pp. 82-95 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@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",

note = "Copyright: Copyright 2020 Elsevier B.V., All rights reserved.; 4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006 ; Conference date: 23-10-2006 Through 26-10-2006",

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",

}

Wang, C, Yang, Z, Ivančić, F & Gupta, A 2006, Whodunit? Causal analysis for counterexamples. in Automated Technology for Verification and Analysis - 4th International Symposium, ATVA 2006, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4218 LNCS, Springer Verlag, pp. 82-95, 4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006, Beijing, China, 10/23/06. https://doi.org/10.1007/11901914_9

Whodunit? Causal analysis for counterexamples. / Wang, Chao; Yang, Zijiang; Ivančić, Franjo; Gupta, Aarti.

Automated Technology for Verification and Analysis - 4th International Symposium, ATVA 2006, Proceedings. Springer Verlag, 2006. p. 82-95 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4218 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Whodunit? Causal analysis for counterexamples

AU - Wang, Chao

AU - Yang, Zijiang

AU - Ivančić, Franjo

AU - Gupta, Aarti

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 -

Wang C, Yang Z, Ivančić F, Gupta A. Whodunit? Causal analysis for counterexamples. In Automated Technology for Verification and Analysis - 4th International Symposium, ATVA 2006, Proceedings. Springer Verlag. 2006. p. 82-95. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/11901914_9