Polymorphic predicate abstraction

ABSTRACT

Predicate abstraction is a technique for creating abstract models of software that are amenable to model checking algorithms. We show how polymorphism, a well-known concept in programming languages and program analysis, can be incorporated in a predicate abstraction algorithm for C programs. The use of polymorphism in predicates, via the introduction of symbolic names for values, allows us to model the effect of a procedure independent of its calling contexts. Therefore, we can safely and precisely abstract a procedure once and then reuse this abstraction across multiple calls and multiple applications containing the procedure. Polymorphism also enables us to handle programs that need to be analyzed in an open environment, for all possible callers. We have proved that our algorithm is sound and have implemented it in the C2BP tool as part of the SLAM software model checking toolkit.

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 , Andreas Podelski , Sriram K. Rajamani, Boolean and Cartesian Abstraction for Model Checking C Programs, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.268-283, April 02-06, 2001
• 3: 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
• 4: 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
• 5: Ball, T. and Rajamani, S. K. 2002a. Generating abstract explanations of spurious counterexamples in C programs. Tech. Rep. MSR-TR-2002-09. Microsoft Research, Jan.
• 6: 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
• 7: Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985 [doi>10.1145/6041.6042]
• 8: 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
• 9: 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]
• 10: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 11: Manuvir Das, Unification-based pointer analysis with directional assignments, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.35-46, June 18-21, 2000, Vancouver, British Columbia, Canada
• 12: Satyaki Das , David L. Dill , Seungjoon Park, Experience with Predicate Abstraction, Proceedings of the 11th International Conference on Computer Aided Verification, p.160-171, July 06-10, 1999
• 13: Detlefs, D., Nelson, G., and Saxe, J. B. 2003. Simplify: A theorem prover for program checking. HP Labs Technical Report HPL-2003-148.
• 14: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 15: Matthew B. Dwyer , John Hatcliff , Roby Joehanes , Shawn Laubach , Corina S. Păsăreanu , Hongjun Zheng , Willem Visser, Tool-supported program abstraction for finite-state verification, Proceedings of the 23rd International Conference on Software Engineering, p.177-187, May 12-19, 2001, Toronto, Ontario, Canada
• 16: Engler, D., Chelf, B., Chou, A., and Hallem, S. 2000. Checking system rules using system-specific, programmer-written compiler extensions. In OSDI 00: Operating System Design and Implementation. Usenix Association.
• 17: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 18: Cormac Flanagan , Shaz Qadeer, Predicate abstraction for software verification, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.191-202, January 16-18, 2002, Portland, Oregon
• 19: Jeffrey S. Foster , Manuel Fähndrich , Alexander Aiken, Polymorphic versus Monomorphic Flow-Insensitive Points-to Analysis for C, Proceedings of the 7th International Symposium on Static Analysis, p.175-198, June 29-July 01, 2000
• 20: 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
• 21: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• 22: Havelund, K. and Pressburger, T. 1998. Model checking Java programs using Java PathFinder. Int. J. Softw. Tools Tech. Trans. 2, 4 (Apr.).
• 23: 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
• 24: 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
• 25: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 26: 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
• 27: William Landi , Barbara G. Ryder, A safe approximate algorithm for interprocedural aliasing, ACM SIGPLAN Notices, v.27 n.7, p.235-248, July 1992
• 28: Milner, R. 1978. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348--375.
• 29: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 30: Morris, J. M. 1982. A general axiom of assignment. In Theoretical Foundations of Programming Methodology. Lecture Notes of an International Summer School, Reidel, pp. 25--34.
• 31: Nelson, G. 1981. Techniques for program verification. Tech. Rep. CSL81-10. Xerox Palo Alto Research Center, Palo Alto, Calif.
• 32: 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]
• 33: Hassen Saïdi , Natarajan Shankar, Abstract and Model Check While You Prove, Proceedings of the 11th International Conference on Computer Aided Verification, p.443-454, July 06-10, 1999
• 34: Sharir, M. and Pnueli, A. 1981. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications. Prentice-Hall, New York, pp. 189--233.
• 35: William Visser , SeungJoon Park , John Penix, Using predicate abstraction to reduce object-oriented programs for model checking, Proceedings of the third workshop on Formal methods in software practice, p.3-182, August 2000, Portland, Oregon, United States [doi>10.1145/349360.351125]
• 36: Robert P. Wilson , Monica S. Lam, Efficient context-sensitive pointer analysis for C programs, Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, p.1-12, June 18-21, 1995, La Jolla, California, United States

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.4 Software/Program Verification
          Subjects: Validation; Reliability

General Terms:
Algorithms, Reliability, Verification

Keywords:
Software model checking, polymorphism, predicate abstraction