Putting static analysis to work for verification: A case study

ABSTRACT

A method for finding bugs in code is presented. For given small numbers j and k, the code of a procedure is translated into a rela-tional formula whose models represent all execution traces that involve at most j heap cells and k loop iterations. This formula is conjoined with the negation of the procedure's specification. The models of the resulting formula, obtained using a constraint solver, are counterexamples: executions of the code that violate the specification.The method can analyze millions of executions in seconds, and thus rapidly expose quite subtle flaws. It can accommodate calls to procedures for which specifications but no code is avail-able. A range of standard properties (such as absence of null pointer dereferences) can also be easily checked, using prede-fined specifications.

REFERENCES

• 1: François Bourdoncle, Abstract debugging of higher-order imperative languages, Proceedings of the ACM SIGPLAN 1993 conference on Programming language design and implementation, p.46-55, June 21-25, 1993, Albuquerque, New Mexico, United States
• 2: 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]
• 3: David R. Chase , Mark Wegman , F. Kenneth Zadeck, Analysis of pointers and structures, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.296-310, June 1990, White Plains, New York, United States
• 4: T.E.Cheatham,Jr.,G.H.Holloway,and J.A.Townley. Symbolic evaluation and the analysis of programs.IEEE Trans. on Softw. Eng.,5(4):402 -417,1979.
• 5: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 6: James C. Corbett, Using shape analysis to reduce finite-state models of concurrent Java programs, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.1, p.51-93, Jan. 2000 [doi>10.1145/332740.332741]
• 7: Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
• 8: L.P.Deutsch.An Interactive Program Verifier PhDthesis,Univ.of California,Berkeley,CA,1973.
• 9: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 10: 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
• 11: Matthew B. Dwyer , Lori A. Clarke, Data flow analysis for verifying properties of concurrent programs, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.62-75, December 06-09, 1994, New Orleans, Louisiana, United States
• 12: Will Dean Gillett, Iterative global flow techniques for detecting program anomalies., 1977
• 13: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• 14: 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]
• 15: C.A.R.Hoare.Recursive data structures.Int. J. of Comp. and Inf. Sci.,4(2):105 -132,1975.
• 16: 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
• 17: James Cornelius King, A program verifier, 1970
• 18: T.Lev-Ami.TVLA:A framework for Kleene based static analysis.Master 's thesis,Tel-Aviv University,2000. Available at http://www.math.tau.ac.il/ ~tla.
• 19: 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
• 20: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 21: J.M.Morris.Assignment and linked data structures.In M.Broy and G.Schmidt,editors,Theoretical Founda-tions of Programming Methodology pages 35 -41.D.Reidel Publishing Co.,Boston,MA,1982.
• 22: Glenford J. Myers, Art of Software Testing, John Wiley & Sons, Inc., New York, NY, 1979
• 23: Kurt M. Olender , Leon J. Osterweil, Cecil: A Sequencing Constraint Language for Automatic Static Analysis Generation, IEEE Transactions on Software Engineering, v.16 n.3, p.268-280, March 1990 [doi>10.1109/32.48935]
• 24: Kurt M. Olender , Leon J. Osterweil, Interprocedural static analysis of sequencing constraints, ACM Transactions on Software Engineering and Methodology (TOSEM), v.1 n.1, p.21-52, Jan. 1992 [doi>10.1145/125489.122822]
• 25: M.Sagiv,T.Reps,and R.Wilhelm.Parametric shape analysis via 3-valued logic.Tech.Rep.TR- 1383,Comp.Sci.Dept.,Univ.of Wisconsin,Madison, WI,August 1998.(Revised March 2000.)Available at "http://www.cs.wisc.edu/wpis/papers/parametric.ps ".
• 26: 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]
• 27: Bjarne Steensgaard, Points-to analysis in almost linear time, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.32-41, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237727]
• 28: Norihisa Suzuki , Kiyoshi Ishihata, Implementation of an array bound checker, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.132-143, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512963]
• 29: M.Tamir.ADI:Automatic derivation of invariants.IEEE Trans. on Softw. Eng.,6(1):40 -48,1990.
• 30: Ben Wegbreit, The synthesis of loop predicates, Communications of the ACM, v.17 n.2, p.102-113, Feb. 1974 [doi>10.1145/360827.360850]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

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

Keywords:
alloy language, constraint solvers, detecting bugs, model checking, relational formulas, static analysis, testing