Article

Termination analysis with calling context graphs

Authors:

Panagiotis Manolios,

Daron VroonAuthors Info & Claims

CAV'06: Proceedings of the 18th international conference on Computer Aided Verification

Pages 401 - 414

https://doi.org/10.1007/11817963_36

Published: 17 August 2006 Publication History

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.

References

[1]

Andrew W. Appel. SSA is functional programming. SIGPLAN Not., 33(4):17-20, 1998.

Digital Library

[2]

Thomas Arts and Jürgen Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236:133-178, 2000.

Digital Library

[3]

Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. Termination of polynomial programs. In Cousot {7}, pages 113-129.

Digital Library

[4]

M. Codish and C. Taboch. A semantic basis for the termination analysis of logic programs. The Journal of Logic Programming, 41(1):103-123, 1999.

[5]

Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Abstraction refinement for termination. In Static Analysis: 12th International Symposium, SAS 2005, volume 3672 of LNCS, pages 87-102, September 2005.

Digital Library

[6]

Patrick Cousot. Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In Cousot {7}, pages 1-24.

Digital Library

[7]

Radhia Cousot, editor. Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings, volume 3385 of Lecture Notes in Computer Science. Springer, 2005.

[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.

Digital Library

[9]

Matt Kaufmann, Panagiotis Manolios, and J Strother Moore, editors. Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, June 2000.

Digital Library

[10]

Matt Kaufmann, Panagiotis Manolios, and J Strother Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, July 2000.

Digital Library

[11]

Matt Kaufmann and J Strother Moore. ACL2 homepage. See URL http://www.cs.- utexas.edu/users/moore/acl2.

[12]

Matt Kaufmann and J. Strother Moore. Structured theory development for a mechanized logic. J. Autom. Reason., 26(2):161-203, 2001.

Digital Library

[13]

Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The size-change principle for program termination. In ACM Symposium on Principles of Programming Languages, volume 28, pages 81-92. ACM Press, 2001.

Digital Library

[14]

Panagiotis Manolios and Daron Vroon. Ordinal arithmetic: Algorithms and mechanization. Journal Of Automated Reasoning. To Appear.

Digital Library

[15]

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.

[16]

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 http://www.cs.utexas.edu/- users/moore/acl2/workshop-2003/.

[17]

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.

[18]

Panagiotis Manolios and Daron Vroon. Integrating static analysis and general-purpose theorem proving for termination analysis. In ICSE'06, The 28th international Conference on Softwar Engineering, Emerging Results. ACM, May 2006.

Digital Library

[19]

Andreas Podelski and Andrey Rybalchenko. A complete method for the synthesis of linear ranking functions. In VMCAI, pages 239-251, 2004.

[20]

A. Tiwari. Termination of linear programs. In R. Alur and D. Peled, editors, Computer-Aided Verification, CAV, volume 3114 of LNCS, pages 70-82. Springer, July 2004.

[21]

Alan Turing. On computable numbers, with an application to the entscheidungsproblem. In Proceedings of the London Mathematical Society, volume 42 of Series 2, pages 230-265, 1936.

Cited By

Muñoz CAyala-Rincón MMoscato MDutle ANarkawicz AAlmeida Ada Silva ARamos T(2023)Formal Verification of Termination Criteria for First-Order Recursive FunctionsJournal of Automated Reasoning10.1007/s10817-023-09669-z67:4Online publication date: 29-Nov-2023
https://dl.acm.org/doi/10.1007/s10817-023-09669-z
Zuleger FGulwani SSinn MVeith H(2011)Bound analysis of imperative programs with the size-change abstractionProceedings of the 18th international conference on Static analysis10.5555/2041552.2041574(280-297)Online publication date: 14-Sep-2011
https://dl.acm.org/doi/10.5555/2041552.2041574
Chamarthi HDillinger PManolios PVroon D(2011)The ACL2 sedan theorem proving systemProceedings of the 17th international conference on Tools and algorithms for the construction and analysis of systems: part of the joint European conferences on theory and practice of software10.5555/1987389.1987424(291-295)Online publication date: 26-Mar-2011
https://dl.acm.org/doi/10.5555/1987389.1987424
Show More Cited By

Recommendations

A methodology for proving termination of general logic programs
A second-order formulation of non-termination

We consider the termination/non-termination property of a class of loops. Such loops are commonly used abstractions of real program pieces. Second-order logic is a convenient language to express non-termination. Of course, such property is generally ...
Cyclic proofs of program termination in separation logic
POPL '08

We propose a novel approach to proving the termination of heap-manipulating programs, which combines separation logic with cyclic proof within a Hoare-style proof system.Judgements in this system express (guaranteed) termination of the program when ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

CAV'06: Proceedings of the 18th international conference on Computer Aided Verification

August 2006

563 pages

ISBN:354037406X

Editors:
Thomas Ball
Microsoft Research, Redmond, WA,
,
Robert B. Jones
Intel Corporation, RA2-459, 2501 W. 229th Avenue, Hillsboro, OR,

Sponsors

INTEL: Intel Corporation
NEC
Cadence Design Systems
Microsoft Research: Microsoft Research
IBM: IBM

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 17 August 2006

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

17
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 22 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Muñoz CAyala-Rincón MMoscato MDutle ANarkawicz AAlmeida Ada Silva ARamos T(2023)Formal Verification of Termination Criteria for First-Order Recursive FunctionsJournal of Automated Reasoning10.1007/s10817-023-09669-z67:4Online publication date: 29-Nov-2023
https://dl.acm.org/doi/10.1007/s10817-023-09669-z
Zuleger FGulwani SSinn MVeith H(2011)Bound analysis of imperative programs with the size-change abstractionProceedings of the 18th international conference on Static analysis10.5555/2041552.2041574(280-297)Online publication date: 14-Sep-2011
https://dl.acm.org/doi/10.5555/2041552.2041574
Chamarthi HDillinger PManolios PVroon D(2011)The ACL2 sedan theorem proving systemProceedings of the 17th international conference on Tools and algorithms for the construction and analysis of systems: part of the joint European conferences on theory and practice of software10.5555/1987389.1987424(291-295)Online publication date: 26-Mar-2011
https://dl.acm.org/doi/10.5555/1987389.1987424
Cook BPodelski ARybalchenko A(2011)Proving program terminationCommunications of the ACM10.1145/1941487.194150954:5(88-98)Online publication date: 1-May-2011
https://dl.acm.org/doi/10.1145/1941487.1941509
Giesl JRaffelsieper MSchneider-Kamp PSwiderski SThiemann R(2011)Automated termination proofs for haskell by term rewritingACM Transactions on Programming Languages and Systems10.1145/1890028.189003033:2(1-39)Online publication date: 7-Feb-2011
https://dl.acm.org/doi/10.1145/1890028.1890030
Spoto FMesnard FPayet É(2010)A termination analyzer for Java bytecode based on path-lengthACM Transactions on Programming Languages and Systems10.1145/1709093.170909532:3(1-70)Online publication date: 1-Mar-2010
https://dl.acm.org/doi/10.1145/1709093.1709095
Ganty PMajumdar RRybalchenko A(2009)Verifying liveness for asynchronous programsACM SIGPLAN Notices10.1145/1594834.148089544:1(102-113)Online publication date: 21-Jan-2009
https://dl.acm.org/doi/10.1145/1594834.1480895
Lee C(2009)Ranking functions for size-change terminationACM Transactions on Programming Languages and Systems10.1145/1498926.149892831:3(1-42)Online publication date: 21-Apr-2009
https://dl.acm.org/doi/10.1145/1498926.1498928
Ganty PMajumdar RRybalchenko AShao ZPierce B(2009)Verifying liveness for asynchronous programsProceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/1480881.1480895(102-113)Online publication date: 21-Jan-2009
https://dl.acm.org/doi/10.1145/1480881.1480895
Cook BPodelski ARybalchenko A(2009)Summarization for terminationFormal Methods in System Design10.1007/s10703-009-0087-835:3(369-387)Online publication date: 1-Dec-2009
https://dl.acm.org/doi/10.1007/s10703-009-0087-8
Show More Cited By

View Options

View options

Figures

Tables

Media

View Table of Conten