Abstract
We introduce calling context graphs and various static and theorem proving based analyses that together provide a powerful method for proving termination of programs written in feature-rich, first order, functional programming languages. In contrast to previous work, our method is highly automated and handles any source of looping behavior in such languages, including recursive definitions, mutual recursion, the use of recursive data structures, etc. We have implemented our method for the ACL2 programming language and evaluated the result using the ACL2 regression suite, which consists of numerous libraries with a total of over 10,000 function definitions. Our method was able to automatically detect termination of over 98% of these functions.
This research was funded in part by NSF grants CCF-0429924, IIS-0417413, and CCF-0438871.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Appel, A.W.: SSA is functional programming. SIGPLAN Not. 33(4), 17–20 (1998)
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236, 133–178 (2000)
Bradley, A.R., Manna, Z., Sipma, H.B.: Termination of polynomial programs. In: Cousot [7], pp. 113–129
Codish, M., Taboch, C.: A semantic basis for the termination analysis of logic programs. The Journal of Logic Programming 41(1), 103–123 (1999)
Cook, B., Podelski, A., Rybalchenko, A.: Abstraction refinement for termination. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 87–102. Springer, Heidelberg (2005)
Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot [7], pp. 1–24
Cousot, R. (ed.): VMCAI 2005. LNCS, vol. 3385. Springer, Heidelberg (2005)
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated termination proofs with AProVE. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 210–220. Springer, Heidelberg (2004)
Kaufmann, M., Manolios, P., Moore, J.S. (eds.): Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, Dordrecht (2000)
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)
Kaufmann, M., Moore, S.: ACL2 homepage, See: http://www.cs.-utexas.edu/users/moore/acl2
Kaufmann, M., Moore, J.S.: Structured theory development for a mechanized logic. J. Autom. Reason. 26(2), 161–203 (2001)
Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: ACM Symposium on Principles of Programming Languages, vol. 28, pp. 81–92. ACM Press, New York (2001)
Manolios, P., Vroon, D.: Ordinal arithmetic: Algorithms and mechanization. Journal of Automated Reasoning (to appear)
Manolios, P., Vroon, D.: Algorithms for ordinal arithmetic. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 243–257. Springer, Heidelberg (2003)
Manolios, P., Vroon, D.: Ordinal arithmetic in ACL2. In: Kaufmann, M., Moore, J.S. (eds.) Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2003) (July 2003), http://www.cs.utexas.edu/-users/moore/acl2/workshop-2003/
Manolios, P., Vroon, D.: Integrating reasoning about ordinal arithmetic into ACL2. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 82–97. Springer, Heidelberg (2004)
Manolios, P., Vroon, D.: Integrating static analysis and general-purpose theorem proving for termination analysis. In: ICSE 2006, The 28th international Conference on Softwar Engineering, Emerging Results. ACM Press, New York (2006)
Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239–251. Springer, Heidelberg (2004)
Tiwari, A.: Termination of linear programs. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 70–82. Springer, Heidelberg (2004)
Turing, A.: On computable numbers, with an application to the entscheidungs problem. In: Proceedings of the London Mathematical Society, vol. 42 of Series 2, pp. 230–265 (1936)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Manolios, P., Vroon, D. (2006). Termination Analysis with Calling Context Graphs. In: Ball, T., Jones, R.B. (eds) Computer Aided Verification. CAV 2006. Lecture Notes in Computer Science, vol 4144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11817963_36
Download citation
DOI: https://doi.org/10.1007/11817963_36
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37406-0
Online ISBN: 978-3-540-37411-4
eBook Packages: Computer ScienceComputer Science (R0)