The pointer assertion logic engine

ABSTRACT

We present a new framework for verifying partial specifications of programs in order to catch type and memory errors and check data structure invariants. Our technique can verify a large class of data structures, namely all those that can be expressed as graph types. Earlier versions were restricted to simple special cases such as lists or trees. Even so, our current implementation is as fast as the previous specialized tools.

Programs are annotated with partial specifications expressed in Pointer Assertion Logic, a new notation for expressing properties of the program store. We work in the logical tradition by encoding the programs and partial specifications as formulas in monadic second-order logic. Validity of these formulas is checked by the MONA tool, which also can provide explicit counterexamples to invalid formulas.

To make verification decidable, the technique requires explicit loop and function call invariants. In return, the technique is highly modular: every statement of a given program is analyzed only once.

The main target applications are safety-critical data-type algorithms, where the cost of annotating a program with invariants is justified by the value of being able to automatically verify complex properties of the program.

REFERENCES

• 1: Krzysztof R. Apt, Ten Years of Hoare's Logic: A Survey—Part I, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.4, p.431-483, Oct. 1981 [doi>10.1145/357146.357150]
• 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: Michael Benedikt , Thomas W. Reps , Shmuel Sagiv, A Decidable Logic for Describing Linked Data Structures, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.2-19, March 22-28, 1999
• 4: Morten Biehl , Nils Klarlund , Theis Rauhe, Algorithms for Guided Tree Automata, Revised Papers from the First International Workshop on Implementing Automata, p.6-25, August 29-31, 1996
• 5: Paul E. Black , Phillip J. Windley, Inference Rules for Programming Languages with Side Effects in Expressions, Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, p.51-60, August 26-30, 1996
• 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: William R. Bush , Jonathan D. Pincus , David J. Sielaff, A static analyzer for finding dynamic programming errors, Software—Practice & Experience, v.30 n.7, p.775-802, June 2000 [doi>10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H]
• 8: Stephen A. Cook , Derek C. Oppen, An assertion language for data structures, Proceedings of the 2nd ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.160-166, January 20-22, 1975, Palo Alto, California [doi>10.1145/512976.512993]
• 9: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Robby, A Language Framework for Expressing Checkable Properties of Dynamic Software, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.205-223, August 30-September 01, 2000
• 10: Thomas T. Cormen , Charles E. Leiserson , Ronald L. Rivest, Introduction to algorithms, MIT Press, Cambridge, MA, 1990
• 11: Patric Cousot. Formal models and semantics. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science volume B, pages 841-993. MIT Press/Elsevier, 1990.
• 12: David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking. Research Report 159, Compaq Systems Research Center, December, 1998.
• 13: Nurit Dor , Michael Rodeh , Shmuel Sagiv, Checking Cleanness in Linked Lists, Proceedings of the 7th International Symposium on Static Analysis, p.115-134, June 29-July 01, 2000
• 14: Jacob Elgaard , Anders Møller , Michael I. Schwartzbach, Compile-Time Debugging of C Programs Working on Trees, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.119-134, April 02, 2000
• 15: David Evans, Static detection of dynamic memory errors, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.44-53, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 16: Robert W. Floyd. Assigning meanings to programs. Mathematical Aspects of Computer Science, American Math. Soc., 1967.
• 17: Pascal Fradet , Ronan Caugne , Daniel Le Métayer, Static Detection of Pointer Errors: An Axiomatisation and a Checking Algorithm, Proceedings of the 6th European Symposium on Programming Languages and Systems, p.125-140, April 22-24, 1996
• 18: Pascal Fradet , Daniel Le Métayer, Shape types, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.27-39, January 15-17, 1997, Paris, France [doi>10.1145/263699.263706]
• 19: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• 20: Klaus Havelund and Thomas Pressburger. Model checking Java programs using Java Path Finder. International Journal on Software Tools for Technology Transf er 2(4), April 2000.
• 21: Laurie J. Hendren , Joseph Hummell , Alexandru Nicolau, Abstractions for recursive pointer data structures: improving the analysis and transformation of imperative programs, Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation, p.249-260, June 15-19, 1992, San Francisco, California, United States
• 22: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 23: Daniel Jackson , Mandana Vaziri, Finding bugs with a constraint solver, Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis, p.14-25, August 21-24, 2000, Portland, Oregon, United States
• 24: Jakob L. Jensen , Michael E. Jørgensen , Michael I. Schwartzbach , Nils Klarlund, Automatic verification of pointer programs using monadic second-order logic, Proceedings of the ACM SIGPLAN 1997 conference on Programming language design and implementation, p.226-234, June 16-18, 1997, Las Vegas, Nevada, United States
• 25: Nils Klarlund, Mona & Fido: The Logic-Automaton Connection in Practice, Selected Papers from the11th International Workshop on Computer Science Logic, p.311-326, August 23-29, 1997
• 26: Nils Klarlund and Anders Moller. MONA Version 1.4 User Manual BRICS Notes Series NS-01-1, Department of Computer Science, University of Aarhus, January 2001.
• 27: Nils Klarlund , Anders Møller , Michael I. Schwartzbach, MONA Implementation Secrets, Revised Papers from the 5th International Conference on Implementation and Application of Automata, p.182-194, July 24-25, 2000
• 28: Nils Klarlund , Michael I. Schwartzbach, Graph types, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.196-205, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158628]
• 29: Nils Klarlund , Michael I. Schwartzbach, Graphs and Decidable Transductions Based on Edge Constraints (Extended Abstract), Proceedings of the 19th International Colloquium on Trees in Algebra and Programming, p.187-201, April 11-13, 1994
• 30: Nils Klarlund , Michael L. Schwartzbach, A Domain-Specific Language for Regular Sets of Strings and Trees, IEEE Transactions on Software Engineering, v.25 n.3, p.378-386, May 1999 [doi>10.1109/32.798326]
• 31: Tal Lev-Ami , Thomas Reps , Mooly Sagiv , Reinhard Wilhelm, Putting static analysis to work for verification: A case study, Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis, p.26-38, August 21-24, 2000, Portland, Oregon, United States
• 32: Tal Lev-Ami , Shmuel Sagiv, TVLA: A System for Implementing Static Analyses, Proceedings of the 7th International Symposium on Static Analysis, p.280-301, June 29-July 01, 2000
• 33: Albert R. Meyer. Wea monadic second-order theory of successor is not elementary recursive. In R. Parikh, editor, Logic Colloquium, (Proc. Symposium on Logic, Boston, 1972), volume 453 of LNCS pages 132-154, 1975.
• 34: Anders Moller. MONA project home page. www.brics.dk/mona
• 35: Anders Moller. PALE project home page. www.brics.dk/PALE
• 36: Joseph M. Morris. A general axiom of assignment. In Theoretical Foundations of Programming Methodology 1982.
• 37: John C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In Millennial Perspectives in Computer Science 2000.
• 38: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.105-118, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292552]
• 39: Thomas R. Shiple , James H. Kukula , Rajeev K. Ranjan, A Comparison of Presburger Engines for EFSM Reachability, Proceedings of the 10th International Conference on Computer Aided Verification, p.280-292, June 28-July 02, 1998

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Frameworks

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming

General Terms:
Design, Languages, Measurement, Performance, Reliability, Theory, Verification