Path slicing

ABSTRACT

We present a new technique, path slicing, that takes as input a possibly infeasible path to a target location, and eliminates all the operations that are irrelevant towards the reachability of the target location. A path slice is a subsequence of the original path whose infeasibility guarantees the infeasibility of the original path, and whose feasibility guarantees the existence of some feasible variant of the given path that reaches the target location even though the given path may itself be infeasible. Our method combines the ability of program slicing to look at several program paths, with the precision that dynamic slicing enjoys by focusing on a single path. We have implemented Path Slicing to analyze possible counterexamples returned by the software model checker Blast. We show its effectiveness in drastically reducing the size of the counterexamples to less than 1% of their original size. This enables the precise verification of application programs (upto 100KLOC), by allowing the analysis to focus on the part of the counterexample that is relevant to the property being checked.

REFERENCES

• 1: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 2: 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
• 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: S. Basu, D. Saha, and S. A. Smolka. Localizing program errors for Cimple debugging. In FORTE 04: Formal Techniques for Networked and Distributed Systems, LNCS 3235, pages 79--96. Springer, 2004.
• 5: Dirk Beyer , Andreas Noack , Claus Lewerentz, Simple and Efficient Relational Querying of Software Structures, Proceedings of the 10th Working Conference on Reverse Engineering, p.216, November 13-17, 2003
• 6: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 7: S. Chaki, J. Ouaknine, K. Yorav, and E. M. Clarke. Automated compositional abstraction refinement for concurrent C programs: A two-level approach. In SoftMC 03: Software Model Checking, 2003.
• 8: Hao Chen , David Wagner, MOPS: an infrastructure for examining security properties of software, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA [doi>10.1145/586110.586142]
• 9: Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 10: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 11: John Field , G. Ramalingam , Frank Tip, Parametric program slicing, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.379-392, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199534]
• 12: C. Flanagan, R. Joshi, X. Ou, and J. B. Saxe. Theorem proving using lazy proof explication. In CAV 03, LNCS, pages 355--367, 2003.
• 13: Cormac Flanagan , James B. Saxe, Avoiding exponential explosion: generating compact verification conditions, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.193-205, January 2001, London, United Kingdom
• 14: Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 15: Grammatech. Codesurfer 1.9. Technical report, 2004.
• 16: A. Groce and W. Visser. What went wrong: Explaining counterexamples. In SPIN 03: SPIN Workshop, LNCS 2648, pages 121--135. Springer, 2003.
• 17: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Kenneth L. McMillan, Abstractions from proofs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.232-244, January 14-16, 2004, Venice, Italy
• 18: 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
• 19: 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]
• 20: 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]
• 21: Ondřej Lhoták , Laurie Hendren, Jedd: a BDD-based relational extension of Java, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 22: Markus Mock , Darren C. Atkinson , Craig Chambers , Susan J. Eggers, Improving program slicing with dynamic points-to data, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA [doi>10.1145/587051.587062]
• 23: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.3, p.217-298, May 2002 [doi>10.1145/514188.514190]
• 24: F. Tip. A survey of program slicing techniques. Journal of Programming Languages, 3:121--189, 1995.
• 25: Mark David Weiser, Program slices: formal, psychological, and practical investigations of an automatic program abstraction method, 1979
• 26: John Whaley , Monica S. Lam, Cloning-based context-sensitive pointer alias analysis using binary decision diagrams, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 27: Xiangyu Zhang , Rajiv Gupta, Cost effective dynamic program slicing, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors

General Terms:
Languages, Reliability, Verification

Keywords:
counterexample analysis, program slicing