A framework for combining analysis and verification

ABSTRACT

We present a general framework for combining program verification and program analysis. This framework enhances program analysis because it takes advantage of user assertions, and it enhances program verification because assertions can be refined using automatic program analysis. Both enhancements in general produce a better way of reasoning about programs than using verification techniques alone or analysis techniques alone. More importantly, the combination is better than simply running the verification and analysis in isolation and then combining the results at the last step. In other words, our framework explores synergistic interaction between verification and analysis. In this paper, we start with a representation of a program, user assertions, and a given analyzer for the program. The framework we describe induces an algorithm which exploits the assertions and the analyzer to produce a generally more accurate analysis. Further, it has some important features: it is flexible: any number of assertions can be used anywhere; it is open: it can employ an arbitrary analyzer; it is modular: we reason with conditional correctness of assertions; it is incremental: it can be tuned for the accuracy/efficiency tradeoff.

REFERENCES

• 1: Manuel Fähndrich , Alexander Aiken, Program Analysis Using Mixed Term and Set Constraints, Proceedings of the 4th International Symposium on Static Analysis, p.114-126, September 08-10, 1997
• 2: Andrew W. Appel, Modern compiler implementation in ML: basic techniques, Cambridge University Press, New York, NY, 1997
• 3: 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]
• 4: 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]
• 5: Patrick Coust, Methods and logics for proving programs, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 6: P. Cousot and R. Cousot. "Abstract Interpretation Frameworks" Journal of Logic and Computation, 2(4), 511-547, August 1992.
• 7: D. Gries, "Science of Programming", Springer-Verlag, 1991.
• 8: Klaus Havelund , Natarajan Shankar, Experiments in Theorem Proving and Model Checking for Protocol Verification, Proceedings of the Third International Symposium of Formal Methods Europe on Industrial Benefit and Advances in Formal Methods, p.662-681, March 18-22, 1996
• 9: Nevin Charles Heintze, Set based program analysis, Carnegie Mellon University, Pittsburgh, PA, 1992
• 10: N. Heintze and J. Jaffar, "A Generic Algorithm for CLP Analysis", 12th International Conference on Logic Programming, 49-63, 1995.
• 11: N. Heintze and J. Jaffar, "An Engine for Logic Program Analysis", Proc. 7th IEEE Syrup. on Logic in Computer Science, pp 318-328, 1992.
• 12: J. Jaffar , J.-L. Lassez, Constraint logic programming, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.111-119, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41635]
• 13: Neil D. Jones , Steven S. Muchnick, A flexible approach to interprocedural data flow analysis and programs with recursive data structures, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.66-74, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582161]
• 14: Greg Nelson , Derek C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.245-257, Oct. 1979 [doi>10.1145/357073.357079]
• 15: Sam Owre , John M. Rushby , Natarajan Shankar, PVS: A Prototype Verification System, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.748-752, June 15-18, 1992
• 16: Vlad Rusu , Eli Singerman, On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.178-192, March 22-28, 1999
• 17: Susanne Graf , Hassen Saïdi, Verifying Invariants Using theorem Proving, Proceedings of the 8th International Conference on Computer Aided Verification, p.196-207, August 03, 1996
• 18: Saddek Bensalem , Yassine Lakhnech , Hassen Saïdi, Powerful Techniques for the Automatic Generation of Invariants, Proceedings of the 8th International Conference on Computer Aided Verification, p.323-335, August 03, 1996

INDEX TERMS

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

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs

General Terms:
Algorithms, Design, Theory

Keywords:
abstract interpretation, program analysis, program verification