Sagar Chaki
Abstract
When a program violates its specification a model checker produces a counterexample that shows an example of undesirable behavior. It is up to the user to understand the error, locate it, and fix the problem. Previous work introduced a technique for explaining and localizing errors based on finding the closest execution to a counterexample, with respect to a distance metric. That approach was applied only to concrete executions of programs. This paper extends and generalizes the approach by combining it with predicate abstraction. Using an abstract state-space increases scalability and makes explanations more informative. Differences between executions are presented in terms of predicates derived from the specification and program, rather than specific changes to variable values. Reasoning to the cause of an error from the factthat in the failing run x < y, but in the successful execution x = y is easier than reasoning from the information that in the failing run y = 239, but in the successful execution y = 232. An abstract explanation is <i>automatically generalized</i>
Predicate abstraction has previously been used in model checking purely as a state-space reduction technique. However, an abstraction good enough to enable a model checking tool to find an error is also likely to be useful as an <i>automatically generated high-level description of a state space</i> --- suitable for use by programmers. Results demonstrating the effectiveness of abstract explanations support this claim.
- F. Aloul, A. Ramani, I. Markov, and K. Sakallah. PBS: A backtrack search pseudo Boolean solver. In Symposium on the theory and applications of satisfiability testing (SAT), pages 346--353, 2002.]]Google Scholar
- B. Alpern, M. Wegman, and F. Zadeck. Detecting equality of variables in programs. In Principles of Programming Languages, pages 1--11, 1988.]] Google ScholarDigital Library
- P. Anderson and T. Teitelbaum. Software inspection using CodeSurfer. In Workshop on Inspection in Software Engineering, 2001.]]Google Scholar
- T. Ball, M. Naik, and S. Rajamani. From symptom to cause: Localizing errors in counterexample traces. In Principles of Programming Languages, pages 97--105, 2003.]] Google ScholarDigital Library
- T. Ball and S. Rajamani. Automatically validating temporal safety properties of interfaces. In SPIN Workshop on Model Checking of Software, pages 103--122, 2001.]] Google ScholarDigital Library
- A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Tools and Algorithms for the Construction and Analysis of Systems, pages 193--207, 1999.]] Google ScholarCross Ref
- S. Chaki, E. Clarke, A. Groce, S. Jha, and H. Veith. Modular verification of software components in C. IEEE Transactions on Software Engineering, 30(6):388--402, 2004.]] Google ScholarDigital Library
- S. Chaki, E. Clarke, A. Groce, and O. Strichman. Predicate abstraction with minimum predicates. In Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), pages 19--34, 2003.]]Google ScholarCross Ref
- E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Computer-Aided Verification, pages 154--169, 2000.]] Google ScholarDigital Library
- E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000.]]Google ScholarDigital Library
- R. Gerth, D. Peled, M. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Protocol Specification Testing and Verification, pages 3--18, 1995.]] Google ScholarDigital Library
- S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In Computer-Aided Verification, pages 72--83, 1997.]] Google ScholarDigital Library
- A. Groce. Error explanation with distance metrics. In Tools and Algorithms for the Construction and Analysis of Systems, pages 108--122, 2004.]]Google ScholarCross Ref
- A. Groce, D. Kroening, and F. Lerda. Understanding counterexamples with explain. In Computer-Aided Verification, 2004. To appear.]]Google ScholarCross Ref
- A. Groce and W. Visser. What went wrong: Explaining counterexamples. In SPIN Workshop on Model Checking of Software, pages 121--135, 2003.]] Google ScholarDigital Library
- T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In Principles of Programming Languages, pages 58--70, 2002.]] Google ScholarDigital Library
- S. Horwitz and T. Reps. The use of program dependence graphs in software engineering. In International Conference of Software Engineering, pages 392--411, 1992.]] Google ScholarDigital Library
- H. Jin, K. Ravi, and F. Somenzi. Fate and free will in error traces. In Tools and Algorithms for the Construction and Analysis of Systems, pages 445--458, 2002.]] Google ScholarDigital Library
- D. Kroening, E. Clarke, and F. Lerda. A tool for checking ANSI-C programs. In Tools and Algorithms for the Construction and Analysis of Systems, pages 168--176, 2004.]]Google Scholar
- D. Lewis. Causation. Journal of Philosophy, 70:556--567, 1973.]]Google ScholarCross Ref
- M. Renieris and S. Reiss. Fault localization with nearest neighbor queries. In Automated Software Engineering, pages 30--39, 2003.]]Google ScholarCross Ref
- G. Rothermel and M. J. Harrold. Empirical studies of a safe regression test selection technique. Software Engineering, 24(6):401--419, 1999.]] Google ScholarDigital Library
- D. Sankoff and J. Kruskal, editors. Time Warps, String Edits, and Macromolecules: the Theory and Practice of Sequence Comparison. Addison Wesley, 1983.]]Google Scholar
- A. Zeller. Isolating cause-effect chains from computer programs. In Foundations of Software Engineering, pages 1--10, 2002.]] Google ScholarDigital Library
- A. Zeller and R. Hildebrandt. Simplifying and isolating failure-inducing input. IEEE Transactions on Software Engineering, 28(2):183--200, 2002.]] Google ScholarDigital Library
Index Terms
- Explaining abstract counterexamples
Recommendations
Explaining abstract counterexamples
SIGSOFT '04/FSE-12: Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineeringWhen a program violates its specification a model checker produces a counterexample that shows an example of undesirable behavior. It is up to the user to understand the error, locate it, and fix the problem. Previous work introduced a technique for ...
Combining Theorem Proving with Model Checking through Predicate Abstraction
This article presents a procedure for proving invariants of infinite-state reactive systems using a combination of two formal verification techniques: theorem proving and model checking. This method uses term rewriting on the definition of the target ...
Formal Verification for C Program
Iterative abstraction refinement has emerged in the last few years as the leading approach to software model checking. We present an approach for automatically verifying C programs against safety specifications based on finite state machine. The ...
Comments