Variance analyses from invariance analyses

ABSTRACT

An invariance assertion for a program location l is a statement that always holds at l during execution of the program. Program invariance analyses infer invariance assertions that can be useful when trying to prove safety properties. We use the term variance assertion to mean a statement that holds between any state at l and any previous state that was also at l. This paper is concerned with the development of analyses for variance assertions and their application to proving termination and liveness properties. We describe a method of constructing program variance analyses from invariance analyses. If we change the underlying invariance analysis, we get a different variance analysis. We describe several applications of the method, including variance analyses using linear arithmetic and shape analysis. Using experimental results we demonstrate that these variance analyses give rise to a new breed of termination provers which are competitive with and sometimes better than today's state-of-the-art termination provers.

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: Andrew W. Appel, Modern Compiler Implementation: In ML, Cambridge University Press, New York, NY, 1998
• 3: J. Berdine, B. Cook, D. Distefano, and P. O'Hearn. Automatic termination proofs for programs with shape-shifting heaps. In CAV'06: International Conference on Computer Aided Verification, 2006.
• 4: A. Biere, C. Artho, and V. Schuppan. Liveness checking as safety checking. In FMICS'02: Formal Methods for Industrial Critical Systems, 2002.
• 5: A. Bradley. Personal communication. Aaron Bradley's suggested script that iteratively applies the tools described in {7} and {6} with increasingly expensive options, June 2006.
• 6: A. Bradley, Z. Manna, and H. Sipma. Termination of polynomial programs. In VMCAI'05: Verification, Model Checking, and Abstract Interpretation, 2005.
• 7: A. R. Bradley, Z. Manna, and H. B. Sipma. The polyranking principle. In ICALP'05: International Colloquium on Automata, Languages and Programming, 2005.
• 8: C. Calcagno, D. Distefano, P. O'Hearn, and H. Yang. Beyond reachability: Shape abstraction in the presence of pointer arithmetic. In SAS'06: Static Analysis Symposium, 2006.
• 9: Michael Colón , Henny Sipma, Synthesis of Linear Ranking Functions, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.67-81, April 02-06, 2001
• 10: Michael Colón , Henny Sipma, Practical Methods for Proving Program Termination, Proceedings of the 14th International Conference on Computer Aided Verification, p.442-454, July 27-31, 2002
• 11: Byron Cook , Alexey Gotsman , Andreas Podelski , Andrey Rybalchenko , Moshe Y. Vardi, Proving that programs eventually do something good, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 12: B. Cook, A. Podelski, and A. Rybalchenko. Abstraction refinement for termination. In SAS'05: Static Analysis Symposium, 2005.
• 13: Byron Cook , Andreas Podelski , Andrey Rybalchenko, Termination proofs for systems code, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 14: B. Cook, A. Podelski, and A. Rybalchenko. Terminator: Beyond safety. In CAV'06: International Conference on Computer Aided Verification, 2006.
• 15: P. Cousot. The calculational design of a generic abstract interpreter. In M. Broy and R. Steinbrüggen, editors, Calculational System Design. 1999.
• 16: P. Cousot. Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In VMCAI'05: Verification, Model Checking, and Abstract Interpretation, 2005.
• 17: P. Cousot. Personal communication, 2006.
• 18: 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]
• 19: 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]
• 20: P. Cousot and R. Cousot. Abstract interpretation frameworks. J. Log. Comput. 2(4), pp511--547, 1992.
• 21: Patrick Cousot , Radhia Cousot, Modular Static Program Analysis, Proceedings of the 11th International Conference on Compiler Construction, p.159-178, April 08-12, 2002
• 22: P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. The ASTRÉE analyzer. In ESOP'05: European Symposium on Programming, 2005.
• 23: Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
• 24: D. Distefano, P. W. O'Hearn, and H. Yang. A local shape analysis based on separation logic. In TACAS'06: Tools and Algorithms for the Construction and Analysis of Systems, 2006.
• 25: R. W. Floyd. Assigning meanings to programs. In Mathematical Aspects of Computer Science, 1967.
• 26: J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke. Automated termination proofs with AProVE. In RTA'04: Rewriting Techniques and Applications, 2004.
• 27: 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
• 28: B. S. Gulavanii and S. K. Rajamani. Counterexample driven refinement for abstract interpretation. In TACAS'06: Tools and Algorithms for the Construction and Analysis of Systems, 2006.
• 29: H. Jain, F. Ivancic, A. Gupta, I. Shlyakhter, and C. Wang. Using statically computed invariants inside the predicate abstraction and refinement loop. In CAV'06: International Conference on Computer Aided Verification, 2006.
• 30: B. Jeannet. NewPolka polyhedra library. http://pop-art.inrialpes.fr/~people/bjeannet/newpolka/index.html.
• 31: Chin Soon Lee , Neil D. Jones , Amir M. Ben-Amram, The size-change principle for program termination, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.81-92, January 2001, London, United Kingdom
• 32: Z. Manna and A. Pnueli. Axiomatic approach to total correctness of programs. Acta Informatica, 1974.
• 33: L. Mauborgne and X. Rival. Trace partitioning in abstract interpretation based static analyzers. In ESOP'05: European Symposium on Programming, 2005.
• 34: A. Miné. The Octagon abstract domain. Higher-Order and Symbolic Computation. (to appear).
• 35: A. Pnueli. The temporal logic of programs. In 18th IEEE Symposium on Foundations of Computer Science, 1977.
• 36: A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In VMCAI'04: Verification, Model Checking, and Abstract Interpretation, 2004.
• 37: Andreas Podelski , Andrey Rybalchenko, Transition Invariants, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), p.32-41, July 13-17, 2004 [doi>10.1109/LICS.2004.50]
• 38: Andreas Podelski , Andrey Rybalchenko, Transition predicate abstraction and fair termination, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.132-144, January 12-14, 2005, Long Beach, California, USA
• 39: John C. Reynolds, The Craft of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• 40: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 41: S. Sankaranarayanan, F. Ivancic, I. Shlyakhter, and A. Gupta. Static analysis in disjunctive numerical domains. In SAS'06: Static Analysis Symposium, 2006.
• 42: A. Tiwari. Termination of linear programs. In CAV'04: International Conference on Computer Aided Verification, 2004.
• 43: M. Y. Vardi. Verification of concurrent programs: The automata-theoretic framework. Ann. Pure Appl. Logic, 51(1-2):79--98, 1991.

INDEX TERMS

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

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

General Terms:
Languages, Reliability, Verification

Keywords:
formal verification, liveness, program analysis, software model checking, termination