Integrating static analysis and general-purpose theorem proving for termination analysis

ABSTRACT

We present emerging results from our work on termination analysis of software systems. We have designed a static analysis algorithm which attains increased precision and flexibility by issuing queries to a theorem prover. We have implemented our algorithm and initial results show that we obtain a significant improvement over the current state-of-the-art in termination analyses. We also outline how our approach, by integrating theorem proving queries into static analyses, can significantly impact the design of general-purpose static analyses.

REFERENCES

• 1: Andrew W. Appel, SSA is functional programming, ACM SIGPLAN Notices, v.33 n.4, p.17-20, April 1998 [doi>10.1145/278283.278285]
• 2: Thomas Arts , Jürgen Giesl, Termination of term rewriting using dependency pairs, Theoretical Computer Science, v.236 n.1-2, p.133-178, April 6, 2000 [doi>10.1016/S0304-3975(99)00207-8]
• 3: 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
• 4: Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. Termination of polynomial programs. In Cousot citeDBLP:conf/vmcai/2005, pages 113--129.
• 5: Patrick Cousot. Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In Cousot citeDBLP:conf/vmcai/2005, pages 1--24.
• 6: Radhia Cousot, editor. Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, volume 3385 of Lecture Notes in Computer Science. Springer, 2005.
• 7: 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
• 8: J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke. Automated termination proofs with AProVE. In Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA-04), volume 3091 of LNCS, pages 210--220. Springer--Verlag, 2004.
• 9: Matt Kaufmann, Panagiotis Manolios, and J Strother Moore, editors. Computer-Aided Reasoning: ACL2 Case Studies Kluwer Academic Publishers, June 2000.
• 10: Matt Kaufmann , J. Strother Moore , Panagiotis Manolios, Computer-Aided Reasoning: An Approach, Kluwer Academic Publishers, Norwell, MA, 2000
• 11: Matt Kaufmann and J Strother Moore. ACL2 homepage. See URL htmlhttp://-www.cs.-utexas.edu/-users/-moore/-acl2.
• 12: 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
• 13: Panagiotis Manolios , Daron Vroon, Ordinal Arithmetic: Algorithms and Mechanization, Journal of Automated Reasoning, v.34 n.4, p.387-423, May 2005 [doi>10.1007/s10817-005-9023-9]
• 14: Panagiotis Manolios and Daron Vroon. Algorithms for ordinal arithmetic. In Franz Baader, editor, 19th International Conference on Automated Deduction -- CADE-19, volume 2741 of LNAI, pages 243--257. Springer--Verlag, July/August 2003.
• 15: Panagiotis Manolios and Daron Vroon. Ordinal arithmetic in ACL2 In Matt Kaufmann and J Strother Moore, editors, Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2003), July 2003. See URL htmlhttp://-www.cs.-utexas.edu/-users/-moore/-acl2/-workshop-2003/.
• 16: Panagiotis Manolios and Daron Vroon. Integrating reasoning about ordinal arithmetic into ACL2. In Formal Methods in Computer-Aided Design: 5th International Conference -- FMCAD-2004, LNCS. Springer--Verlag, November 2004.
• 17: Andreas Podelski and Andrey Rybalchenko. A complete method for the synthesis of linear ranking functions. In Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, volume 2937 of Lecture Notes in Computer Science, pages 239--251. Springer, 2004.
• 18: Reneé Thiemann and Jürgen Giesl. Size-change termination for term rewriting. Technical Report AIB-2003-02, RWTH Aachen, January 2003.

INDEX TERMS

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

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic

General Terms:
Algorithms, Verification

Keywords:
ACL2, liveness, static analysis, termination, theorem proving