Explaining abstract counterexamples

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.

REFERENCES

• 1: 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.
• 2: B. Alpern , M. N. Wegman , F. K. Zadeck, Detecting equality of variables in programs, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-11, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73561]
• 3: P. Anderson and T. Teitelbaum. Software inspection using CodeSurfer. In Workshop on Inspection in Software Engineering, 2001.
• 4: Thomas Ball , Mayur Naik , Sriram K. Rajamani, From symptom to cause: localizing errors in counterexample traces, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.97-105, January 15-17, 2003, New Orleans, Louisiana, USA
• 5: Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
• 6: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 7: Modular Verification of Software Components in C, IEEE Transactions on Software Engineering, v.30 n.6, p.388-402, June 2004 [doi>10.1109/TSE.2004.22]
• 8: 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.
• 9: Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, p.154-169, July 15-19, 2000
• 10: E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000.
• 11: Rob Gerth , Doron Peled , Moshe Y. Vardi , Pierre Wolper, Simple on-the-fly automatic verification of linear temporal logic, Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification XV, p.3-18, June 01, 1995
• 12: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 13: A. Groce. Error explanation with distance metrics. In Tools and Algorithms for the Construction and Analysis of Systems, pages 108--122, 2004.
• 14: A. Groce, D. Kroening, and F. Lerda. Understanding counterexamples with explain. In Computer-Aided Verification, 2004. To appear.
• 15: A. Groce and W. Visser. What went wrong: Explaining counterexamples. In SPIN Workshop on Model Checking of Software, pages 121--135, 2003.
• 16: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 17: Susan Horwitz , Thomas Reps, The use of program dependence graphs in software engineering, Proceedings of the 14th international conference on Software engineering, p.392-411, May 11-15, 1992, Melbourne, Australia [doi>10.1145/143062.143156]
• 18: HoonSang Jin , Kavita Ravi , Fabio Somenzi, Fate and Free Will in Error Traces, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.445-459, April 08-12, 2002
• 19: 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.
• 20: D. Lewis. Causation. Journal of Philosophy, 70:556--567, 1973.
• 21: M. Renieris and S. Reiss. Fault localization with nearest neighbor queries. In Automated Software Engineering, pages 30--39, 2003.
• 22: Gregg Rothermel , Mary Jean Harrold, Empirical Studies of a Safe Regression Test Selection Technique, IEEE Transactions on Software Engineering, v.24 n.6, p.401-419, June 1998 [doi>10.1109/32.689399 ]
• 23: D. Sankoff and J. Kruskal, editors. Time Warps, String Edits, and Macromolecules: the Theory and Practice of Sequence Comparison. Addison Wesley, 1983.
• 24: Andreas Zeller, Isolating cause-effect chains from computer programs, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA [doi>10.1145/587051.587053]
• 25: Andreas Zeller , Ralf Hildebrandt, Simplifying and Isolating Failure-Inducing Input, IEEE Transactions on Software Engineering, v.28 n.2, p.183-200, February 2002 [doi>10.1109/32.988498 ]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Verification

Keywords:
fault localization, model checking, predicate abstraction