From symptom to cause: localizing errors in counterexample traces

ABSTRACT

There is significant room for improving users' experiences with model checking tools. An error trace produced by a model checker can be lengthy and is indicative of a symptom of an error. As a result, users can spend considerable time examining an error trace in order to understand the cause of the error. Moreover, even state-of-the-art model checkers provide an experience akin to that provided by parsers before syntactic error recovery was invented: they report a single error trace per run. The user has to fix the error and run the model checker again to find more error traces.We present an algorithm that exploits the existence of correct traces in order to localize the error cause in an error trace, report a single error trace per error cause, and generate multiple error traces having independent causes. We have implemented this algorithm in the context of slam, a software model checker that automatically verifies temporal safety properties of C programs, and report on our experience using it to find and localize errors in device drivers. The algorithm typically narrows the location of a cause down to a few lines, even in traces consisting of hundreds of statements.

REFERENCES

• 1: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 2: Thomas Ball , Sriram K. Rajamani, Bebop: A Symbolic Model Checker for Boolean Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.113-130, August 30-September 01, 2000
• 3: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 4: Mike Beaven , Ryan Stansifer, Explaining type errors in polymorphic languages, ACM Letters on Programming Languages and Systems (LOPLAS), v.2 n.1-4, p.17-30, March–Dec. 1993 [doi>10.1145/176454.176460]
• 5: Karthikeyan Bhargavan , Carl A. Gunter , Insup Lee , Oleg Sokolsky , Moonjoo Kim , Davor Obradovic , Mahesh Viswanathan, Verisim: Formal Analysis of Network Simulations, IEEE Transactions on Software Engineering, v.28 n.2, p.129-145, February 2002 [doi>10.1109/32.988495]
• 6: Olaf Chitil, Compositional explanation of types and algorithmic debugging of type errors, Proceedings of the sixth ACM SIGPLAN international conference on Functional programming, September 03-05, 2001, Florence, Italy
• 7: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 8: Dominic Duggan , Frederick Bent, Explaining type inference, Science of Computer Programming, v.27 n.1, p.37-83, July 1996 [doi>10.1016/0167-6423(95)00007-0]
• 9: Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically Discovering Likely Program Invariants to Support Program Evolution, IEEE Transactions on Software Engineering, v.27 n.2, p.99-123, February 2001 [doi>10.1109/32.908957]
• 10: A. Groce and W. Visser. What went wrong: Explaining counterexamples. Technical Report 02-08, RIACS, USRA, 2002.
• 11: Seth Hallem , Benjamin Chelf , Yichen Xie , Dawson Engler, A system and language for building system-specific, static analyses, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 12: Sudheendra Hangal , Monica S. Lam, Tracking down software bugs using automatic anomaly detection, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581377]
• 13: Gerard J. Holzmann, Logic Verification of ANSI-C Code with SPIN, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.131-147, August 30-September 01, 2000
• 14: Susan Horwitz , Thomas Reps , David Binkley, Interprocedural slicing using dependence graphs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.1, p.26-60, Jan. 1990 [doi>10.1145/77606.77608]
• 15: 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
• 16: Gregory F. Johnson , Janet A. Walz, A maximum-flow approach to anomaly isolation in unification-based incremental type inference, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.44-57, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512649]
• 17: B. Korel , J. Laski, Dynamic program slicing, Information Processing Letters, v.29 n.3, p.155-163, October 26, 1988 [doi>10.1016/0020-0190(88)90054-3]
• 18: Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
• 19: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multithreaded programs, ACM Transactions on Computer Systems (TOCS), v.15 n.4, p.391-411, Nov. 1997 [doi>10.1145/265924.265927]
• 20: Ehud Y. Shapiro, Algorithmic Program DeBugging, MIT Press, Cambridge, MA, 1983
• 21: Oleg Sheyner , Joshua Haines , Somesh Jha , Richard Lippmann , Jeannette M. Wing, Automated Generation and Analysis of Attack Graphs, Proceedings of the 2002 IEEE Symposium on Security and Privacy, p.273, May 12-15, 2002
• 22: F. Tip , T. B. Dinesh, A slicing-based approach for locating type errors, ACM Transactions on Software Engineering and Methodology (TOSEM), v.10 n.1, p.5-55, Jan. 2001 [doi>10.1145/366378.366379]
• 23: Mitchell Wand, Finding the source of type errors, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.38-43, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512648]
• 24: M. Weiser. Program slicing. IEEE Transactions on Software Engineering, SE-10(4):352--357, July 1984.
• 25: Andreas Zeller, Yesterday, my program worked. Today, it does not. Why?, Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, p.253-267, September 06-10, 1999, Toulouse, France

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Algorithms, Verification

Keywords:
debugging, software model checking