article

Open access

Program termination analysis in polynomial time

Authors:

Amir M. Ben-Amram,

Chin Soon LeeAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 29, Issue 1

Article No.: 5, Pages 1 - 37

https://doi.org/10.1145/1180475.1180480

Published: 01 January 2007 Publication History

Abstract

A size-change termination algorithm takes as input abstract information about a program in the form of size-change graphs and uses it to determine whether any infinite computation would imply that some data decrease in size infinitely. Since such an infinite descent is presumed impossible, this proves program termination. The property of the graphs that implies program termination is called SCT. There are many examples of practical programs whose termination can be verified by creating size-change graphs and testing them for SCT.The size-change graph abstraction is useful because the graphs often carry sufficient information to deduce termination, and at the same time are simple enough to be analyzed automatically. However, there is a tradeoff between the completeness and efficiency of this analysis, and complete algorithms in the literature can easily be pushed to an exponential combinatorial search by certain patterns in the graph structures.We therefore propose a novel algorithm to detect common forms of parameter-descent behavior efficiently. Specifically, we target lexicographic descent, multiset descent, and min- and max-descent. Our algorithm makes it possible to verify practical instances of SCT while guarding against unwarranted combinatorial search. It has worst-case time complexity cubic in the input size, and its effectiveness is demonstrated empirically using a test suite of over 90 programs.

References

[1]

Anderson, H. and Khoo, S. C. 2003. Affine-Based size-change termination. In Proceedings of the 1st Asian Symposium on Programming Languages and Systems (APLAS), A. Ohori, Ed. Lecture Notes in Computer Science, vol. 2895. Springer Verlag, 122--140.

[2]

Anderson, H. and Khoo, S. C. 2005. Bounded size-change termination. Tech. Rep. TRB6/05, National University of Singapore, Singapore.

[3]

Apt, K. R. and Pedreschi, D. 1994. Modular termination proofs for logic and pure Prolog programs. In Advances in Logic Programming Theory. Oxford University Press, 183--229.

Digital Library

[4]

Arts, T. 2001. Automatically proving termination and innermost normalisation of term rewriting systems. Ph.D. thesis, Universiteit Utrecht, The Netherlands.

Digital Library

[5]

Avery, J. 2005. The size-change termination principle on non well founded data types. Tech. Rep., Datalogisk Institut Københavns Universitet, Denmark.

[6]

Ben-Amram, A. 2002. General size-change termination and lexicographic descent. In The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, T. Mogensen et al. Eds. Lecture Notes in Computer Science, vol. 2566. Springer Verlag, 3--17.

Digital Library

[7]

Bueno, F., García de la Banda, M., and Hermenegildo, M. 1994. Effectiveness of global analysis in strict independence-based automatic program parallelization. In Proceedings of the International Logic Programming Symposium (ILPS). MIT Press, Cambridge, MA. 320--336.

Digital Library

[8]

Codish, M., Lagoon, V., and Stuckey, P. 2005. Testing for termination with monotonicity constraints. In Proceedings of the 21st International Conference on Logic Programming (ICLP). To appear.

Digital Library

[9]

Codish, M., Mariott, K., and Taboch, C. 2000. Improving program analyses by structure untupling. J. Logic Program. 43, 3, 251--263.

[10]

Codish, M. and Taboch, C. 1997. A semantic basis for termination analysis of logic programs and its realization using symbolic norm constraints. In Proceedings of the 6th International Conference on Algebraic and Logic Programming (ALP), M. Hanus et al., Eds. Lecture Notes in Computer Science, vol. 1298. Springer Verlag, 31--45.

Digital Library

[11]

Cormen, T. H., Leiserson, C. E., and Rivest, R. L. 2001. Introduction to Algorithms. MIT Press Cambridge, MA.

Digital Library

[12]

Dershowitz, N. and Manna, Z. 1979. Proving termination with multiset orderings. Commun. ACM 22, 8 (Aug.), 465--476.

Digital Library

[13]

De Schreye, D. and Decorte, S. 1994. Termination of logic programs: The never-ending story. J. Logic Program. 19--20, 199--260.

[14]

Floyd, R. W. 1967. Assigning meanings to programs. Proceedings of Symposia in Applied Mathematics XIX, 19--32.

[15]

Frederiksen, C. C. 2001. A simple implementation of the size-change principle. Tech. Rep. D-442, Datalogisk Institut Københavns Universitet, Denmark.

[16]

Genaim, S. and Codish, M. 2002. Combining norms to prove termination. In Proceedings of the International Workshop on Verification, Model Checking and Abstract Interpretation (VMCAI). Springer Verlag.

Digital Library

[17]

Giesl, J., Thiemann, R., Schneider-Kamp, P., and Falke, S. 2004. Automated termination proofs with AProVE. In Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, vol. 3091. Springer Verlag, 210--220.

Digital Library

[18]

Glenstrup, A. and Jones, N. 2004. Termination analysis and specialization-point insertion in off-line partial evaluation. Tech. Rep. D-498, Datalogisk Institut Københavns Universitet, Denmark.

[19]

Jones, N. D. and Bohr, N. 2004. Termination analysis of the untyped lambda calculus. In Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, vol. 3091. Springer Verlag, 1--23.

[20]

Lee, C. S. 1999. Partial evaluation of the Euclidean algorithm, revisited. Higher-Order Symb. Comput. 12, 2 (Sept.), 203--212.

Digital Library

[21]

Lee, C. S. 2001. Program termination analysis and termination of offline partial evaluation. Ph.D. thesis, UWA, Australia.

Digital Library

[22]

Lee, C. S., Jones, N. D., and Ben-Amram, A. 2001. The size-change principle for program termination. In Proceedings of the 28th ACM Symposium on Principles of Programming Languages (POPL).

Digital Library

[23]

Lee, C. S. 2002. Program termination analysis in polynomial time. In Proceedings of the 1st International Conference on Generative Programming and Component Engineering (GPCE). Lecture Notes in Computer Science, vol. 2487. Sringer Verlag, 218--235.

Digital Library

[24]

Lindenstrauss, N. and Sagiv, Y. 1997a. Automatic termination analysis of logic programs (with detailed experimental results). http://www.cs.huji.ac.il/~naomil/.

[25]

Lindenstrauss, N. and Sagiv, Y. 1997b. Automatic termination analysis of Prolog programs. In Proceedings of the 14th International Conference on Logic Programming (ICLP), L. Naish, Ed. MIT Press, Cambridge, MA. 64--77.

[26]

Paige, R. and Yang, Z. 1997. High level reading and structure compilation. In Proceedings of the 24th ACM Symposium on Principles of Programming Languages (POPL). 456--469.

Digital Library

[27]

Péter, R. 1967. Recursive Functions. Academic Press.

[28]

Plümer, L. 1990. Termination Proofs for Logic Programs. Lecture Notes in Artificial Intelligence, vol. 446. Springer Verlag.

Digital Library

[29]

Podelski, A. and Rybalchenko, A. 2005. Transition predicate abstraction and fair termination. In Proceedings of the 32nd ACM Symposium on Principles of Programming Languages (POPL).

Digital Library

[30]

Sagiv, Y. 1991. A termination test for logic programs. In Proceedings of the International Logic Programming Symposium (ILPS), V. Saraswat and K. Ueda, Eds. MIT Press, Cambridge, MA. 518--532.

[31]

Thiemann, R. and Giesl, J. 2003. Size-Change termination for term rewriting. In Proceedings of the 14th International Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, vol. 2706. Springer Verlag, 264--278.

Digital Library

[32]

Thiemann, R. and Giesl, J. 2005. The size-change principle and dependency pairs for termination of term rewriting. In Applicable Algebra in Engineering, Communication and Computing. To appear. doi 10.1007/s00200-005-0179-7.

[33]

Turing, A. M. 1948. Checking a large routine. In Report of a Conference on High Speed Automatic Calculating Machines. 67--69. Reprinted in The Early British Computer Conferences, vol. 14 of Charles Babbage Institute Reprint Series For The History Of Computing, MIT Press, Cambridge, MA. 1989.

Digital Library

[34]

Wahlstedt, D. 2000. Detecting termination using size-change in parameter values. Master's thesis, Göteborgs Universitet, Sweden.

[35]

Xi, H. 1999. Dependent types for program termination verification. Higher-Order Symb. Comput. 15, 1 (Mar.), 91--131.

Digital Library

Cited By

Cohen LJabarin APopescu ARowe R(2024)The Complex(ity) Landscape of Checking Infinite DescentProceedings of the ACM on Programming Languages10.1145/36328888:POPL(1352-1384)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632888
Hainry EKapron BMarion JPéchoux R(2022)Complete and tractable machine-independent characterizations of second-order polytimeFoundations of Software Science and Computation Structures10.1007/978-3-030-99253-8_19(368-388)Online publication date: 29-Mar-2022
https://doi.org/10.1007/978-3-030-99253-8_19
Sinn MZuleger FVeith H(2017)Complexity and Resource Bound Analysis of Imperative Programs Using Difference ConstraintsJournal of Automated Reasoning10.1007/s10817-016-9402-459:1(3-45)Online publication date: 1-Jun-2017
https://dl.acm.org/doi/10.1007/s10817-016-9402-4
Show More Cited By

Index Terms

Program termination analysis in polynomial time

Recommendations

Size-change termination with difference constraints

This article considers an algorithmic problem related to the termination analysis of programs. More specifically, we are given bounds on differences in sizes of data values before and after every transition in the program's control-flow graph. Our goal ...
Ranking functions for size-change termination

This article explains how to construct a ranking function for any program that is proved terminating by size-change analysis.

The “principle of size-change termination” for a first-order functional language with well-ordered data is intuitive: A program ...
Proving termination of context-sensitive rewriting by transformation

Context-sensitive rewriting (CSR) is a restriction of rewriting that forbids reductions on selected arguments of functions. With CSR, we can achieve a terminating behavior with non-terminating term rewriting systems, by pruning (all) infinite rewrite ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 29, Issue 1

January 2007

273 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/1180475

Issue’s Table of Contents

Copyright © 2007 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 2007

Published in TOPLAS Volume 29, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

31
Total Citations
View Citations
799
Total Downloads

Downloads (Last 12 months)87
Downloads (Last 6 weeks)14

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Cohen LJabarin APopescu ARowe R(2024)The Complex(ity) Landscape of Checking Infinite DescentProceedings of the ACM on Programming Languages10.1145/36328888:POPL(1352-1384)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632888
Hainry EKapron BMarion JPéchoux R(2022)Complete and tractable machine-independent characterizations of second-order polytimeFoundations of Software Science and Computation Structures10.1007/978-3-030-99253-8_19(368-388)Online publication date: 29-Mar-2022
https://doi.org/10.1007/978-3-030-99253-8_19
Sinn MZuleger FVeith H(2017)Complexity and Resource Bound Analysis of Imperative Programs Using Difference ConstraintsJournal of Automated Reasoning10.1007/s10817-016-9402-459:1(3-45)Online publication date: 1-Jun-2017
https://dl.acm.org/doi/10.1007/s10817-016-9402-4
Leuschel MVidal G(2014)Fast offline partial evaluation of logic programsInformation and Computation10.1016/j.ic.2014.01.005235(70-97)Online publication date: 1-Apr-2014
https://dl.acm.org/doi/10.1016/j.ic.2014.01.005
Fogarty SVardi M(2012)BÃ¼chi Complementation and Size-Change TerminationLogical Methods in Computer Science10.2168/LMCS-8(1:13)20128:1Online publication date: 27-Feb-2012
https://doi.org/10.2168/LMCS-8(1:13)2012
Ben-Amram AGenaim SMasud A(2012)On the Termination of Integer LoopsACM Transactions on Programming Languages and Systems10.1145/2400676.240067934:4(1-24)Online publication date: 1-Dec-2012
https://dl.acm.org/doi/10.1145/2400676.2400679
Xu DKiselyov OThompson S(2012)Hybrid contract checking via symbolic simplificationProceedings of the ACM SIGPLAN 2012 workshop on Partial evaluation and program manipulation10.1145/2103746.2103767(107-116)Online publication date: 23-Jan-2012
https://dl.acm.org/doi/10.1145/2103746.2103767
Ben-Amram AGenaim SMasud A(2012)On the termination of integer loopsProceedings of the 13th international conference on Verification, Model Checking, and Abstract Interpretation10.1007/978-3-642-27940-9_6(72-87)Online publication date: 22-Jan-2012
https://dl.acm.org/doi/10.1007/978-3-642-27940-9_6
Peña RDelgado-Muñoz A(2011)Size invariant and ranking function synthesis in a functional languageProceedings of the 20th international conference on Functional and constraint logic programming10.5555/2032603.2032609(52-67)Online publication date: 19-Jul-2011
https://dl.acm.org/doi/10.5555/2032603.2032609
Ben-Amram A(2011)Monotonicity Constraints for Termination in the Integer DomainLogical Methods in Computer Science10.2168/LMCS-7(3:4)20117:3Online publication date: 24-Aug-2011
https://doi.org/10.2168/LMCS-7(3:4)2011
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents