Isil Dillig
Alex Aiken
ABSTRACT
When program verification tools fail to verify a program, either the program is buggy or the report is a false alarm. In this situation, the burden is on the user to manually classify the report, but this task is time-consuming, error-prone, and does not utilize facts already proven by the analysis. We present a new technique for assisting users in classifying error reports. Our technique computes small, relevant queries presented to a user that capture exactly the information the analysis is missing to either discharge or validate the error. Our insight is that identifying these missing facts is an instance of the abductive inference problem in logic, and we present a new algorithm for computing the smallest and most general abductions in this setting. We perform the first user study to rigorously evaluate the accuracy and effort involved in manual classification of error reports. Our study demonstrates that our new technique is very useful for improving both the speed and accuracy of error report classification. Specifically, our approach improves classification accuracy from 33% to 90% and reduces the time programmers take to classify error reports from approximately 5 minutes to under 1 minute.
- Bessey, A., Block, K., Chelf, B., Chou, A., Fulton, B., Hallem, S., Henri-Gros, C., Kamsky, A., McPeak, S., Engler, D.: A few billion lines of code later: using static analysis to find bugs in the real world. Communications of the ACM 53(2) (2010) 66--75 Google Scholar
Digital Library
- Dillig, I., Dillig, T., Aiken, A.: Automated error diagnosis using abductive inference (extended version). http://www.cs.wm.edu/~idillig/pldi12-extended.pdfGoogle Scholar
- Dillig, I., Dillig, T., McMillan, K., Aiken, A.: Minimum satisfying assignments for SMT. In: To appear in CAV. (2012) Google ScholarDigital Library
- Dillig, I., Dillig, T., Aiken, A.: Small formulas for large programs: On-line constraint simplification in scalable static analysis. Static Analysis Symposium (SAS) (2010) 236--252 Google ScholarDigital Library
- Dillig, I., Dillig, T., Aiken, A.: Fluid updates: Beyond strong vs. weak updates. ESOP (2010) 246--266 Google ScholarDigital Library
- Dillig, I., Dillig, T., Aiken, A.: Precise reasoning for programs using containers. POPL (2011) 187--200 Google ScholarDigital Library
- Dillig, I., Dillig, T., Aiken, A., Sagiv, M.: Precise and compact modular procedure summaries for heap manipulating programs. In: PLDI. (2011) 567--577 Google ScholarDigital Library
- Ball, T., Naik, M., Rajamani, S.: From symptom to cause: localizing errors in counterexample traces. POPL 38(1) (2003) 97--105 Google ScholarDigital Library
- Groce, A.: Error explanation with distance metrics. TACAS (2004) 108--122Google Scholar
- Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. In: PLDI, ACM (2011) 437--446 Google ScholarDigital Library
- Griesmayer, A., Staber, S., Bloem, R.: Automated fault localization for c programs. Theoretical Computer Science 174(4) (2007) 95--111 Google ScholarDigital Library
- Renieres, M., Reiss, S.: Fault localization with nearest neighbor queries. In: ASE. (2003) 30--39Google Scholar
- Ravi, K., Somenzi, F.: Minimal assignments for bounded model checking. TACAS (2004) 31--45Google Scholar
- Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Software verification with blast. Model Checking Software (2003) 624--624 Google ScholarDigital Library
- Ball, T., Rajamani, S.: The SLAM project: debugging system software via static analysis. In: POPL, NY, USA (2002) 1--3 Google ScholarDigital Library
- Henzinger, T., Jhala, R., Majumdar, R., McMillan, K.: Abstractions from proofs. POPL 39(1) (2004) 232--244 Google ScholarDigital Library
- Manevich, R., Sridharan, M., Adams, S., Das, M., Yang, Z.: PSE: explaining program failures via postmortem static analysis. In: FSE. Volume 29., ACM (2004) 63--72 Google ScholarDigital Library
- Le, W., Soffa, M.: Path-based fault correlations. In: FSE. (2010) 307--316 Google ScholarDigital Library
- Weimer, W.: Patches as better bug reports. In: GPCE. (2006) 181--190 Google ScholarDigital Library
- Weiser, M.: Program slicing. In: ICSE, IEEE Press (1981) 439--449 Google ScholarDigital Library
- Korel, B., Laski, J.: Dynamic program slicing. Information Processing Letters 29(3) (1988) 155--163 Google ScholarDigital Library
- Sridharan, M., Fink, S., Bodik, R.: Thin slicing. In: PLDI, ACM (2007) 112--122 Google ScholarDigital Library
- Beaven, M., Stansifer, R.: Explaining type errors in polymorphic languages. LOPLAS 2(1--4) (1993) 17--30 Google ScholarDigital Library
- Haack, C., Wells, J.: Type error slicing in implicitly typed higher-order languages. Programming Languages and Systems (2003) 284--301 Google ScholarDigital Library
- Yang, J.: Explaining type errors by finding the source of a type conflict. Trends in Functional Programming (1999) 49--57 Google ScholarDigital Library
- Lerner, B., Flower, M., Grossman, D., Chambers, C.: Searching for type-error messages. In: PLDI, ACM (2007) 425--434 Google ScholarDigital Library
- Nori, A., Rajamani, S., Tetali, S., Thakur, A.: The yogi project: Software property checking via static analysis and testing. TACAS (2009) 178--181 Google ScholarDigital Library
- Godefroid, P., Nori, A., Rajamani, S., Tetali, S.: Compositional may-must program analysis: unleashing the power of alternation. In: POPL. Volume 45., ACM (2010) 43--56 Google ScholarDigital Library
- Yorsh, G., Ball, T., Sagiv, M.: Testing, abstraction, theorem proving: better together! In: ISSTA, ACM (2006) 145--156 Google ScholarDigital Library
- Dillig, I., Dillig, T., Aiken, A.: Sound, complete and scalable path-sensitive analysis. In: PLDI, ACM (2008) 270--280 Google ScholarDigital Library
Index Terms
- Automated error diagnosis using abductive inference
Recommendations
Automated error diagnosis using abductive inference
PLDI '12When program verification tools fail to verify a program, either the program is buggy or the report is a false alarm. In this situation, the burden is on the user to manually classify the report, but this task is time-consuming, error-prone, and does ...
Fast Error Diagnosis for Combinational Verification
VLSID '00: Proceedings of the 13th International Conference on VLSI DesignWe address the problem of localizing error sites in a combinational circuit that has been shown to be inequivalent to its specification. In the typical case, it is not possible to identify the error location exactly. We propose a novel diagnosis ...
Reachability and error diagnosis in LR(1) parsers
CC 2016: Proceedings of the 25th International Conference on Compiler ConstructionGiven an LR(1) automaton, what are the states in which an error can be detected? For each such "error state", what is a minimal input sentence that causes an error in this state? We propose an algorithm that answers these questions. This allows ...
Comments