Article

Practical Methods for Proving Program Termination

Authors:

Michael Colón,

Henny SipmaAuthors Info & Claims

CAV '02: Proceedings of the 14th International Conference on Computer Aided Verification

Pages 442 - 454

Published: 27 July 2002 Publication History

Abstract

We present two algorithms to prove termination of programs by synthesizing linear ranking functions. The first uses an invariant generator based on iterative forward propagation with widening and extracts rankingf unctions from the generated invariants by manipulating polyhedral cones. It is capable of finding subtle ranking functions which are linear combinations of many program variables, but is limited to programs with few variables.The second, more heuristic, algorithm targets the class of structured programs with single-variable ranking functions. Its invariant generator uses a heuristic extrapolation operator to avoid iterative forward propagation over program loops. For the programs we have considered, this approach converges faster and the invariants it discovers are sufficiently strong to imply the existence of ranking functions.

References

[1]

Nikolaj S. Bjørner, Anca Browne, Michael Colón, Bernd Finkbeiner, Zohar Manna, Henny B. Sipma, and Tomás E. Uribe. Verifying temporal properties of reactive systems: A STeP tutorial. Formal Methods in System Design , 16(3):227-270, June 2000.

[2]

J. Brauburger and J. Giesl. Approximating the domains of functional and imperative programs. Science of Computer Programming , 35:113-136, 1999.

[3]

G. E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In H. Brakhage, editor, Proc. Second GI Conf. Autamata Theory and Formal Languages , volume 33 of Lecture Notes in Computer Science , pag es 134-183, 1975.

[4]

Michael Colón and Henny Sipma. Synthesis of linear ranking functions. In Tiziana Margaria and Wang Yi, editors, 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) , volume 2031 of LNCS , pages 67-81. Springer Verlag, April 2001.

[5]

T. Cormen, C. Leiserson, and R. Rivest. Introduction to Algorithms . McGraw-Hill, New York, 1990.

[6]

Patrick Cousot and Rhadia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4 th ACM Symp. Princ. of Prog. Lang. , pages 238-252. ACM Press, 1977.

[7]

Patrick Cousot and Nicholas Halbwachs. Automatic discovery of linear restraints among the variables of a program. In 5 th ACM Symp. Princ. of Prog. Lang. , pages 84-97, January 1978.

[8]

Dennis Dams, Rob Gerth, and Orna Grumberg. A heuristic for the automatic generation of ranking functions. In Workshop on Advances in Verification (WAVe'00) , pages 1-8, 2000.

[9]

N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation , 3:69- 116, 1987.

[10]

K. Fukuda and A. Prodon. Double description method revisited. In Combinatorics and Computer Science , volume 1120 of Lecture Notes in Computer Science , pages 91-111. Springer-Verlag, 1996.

[11]

J. Giesl. Generating polynomial orderings for termination proofs. In J. Hsiang, editor, Proc. 6th Intl. Conf. Rewriting Techniques and Applications , volume 914 of Lecture Notes in Computer Science , pages 426-431. Springer-Verlag, 1995.

[12]

J. Giesl, C. Walther, and J. Brauburger. Termination analysis for functional programs. In W. Bibel and P. H. Schmitt, editors, Automated Deduction - A Basis for Applications, Volume III: Applications , chapter 6, pages 135-164. Kluwer Academic, 1998.

[13]

Zohar Manna. Mathematical Theory of Computation . McGraw-Hill, 1974.

[14]

Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems: Safety . Springer-Verlag, New York, 1995.

[15]

D. de Schreye and S. Decorte. Termination of logic programs: The never ending story. Journal of Logic Programming , 19, 20:199-260, 1994.

[16]

Niklaus Wirth. Algorithms + Data Structures = Programs . Prentice-Hall, 1976.

Cited By

Borralleras CLarraz DRodríguez-Carbonell EOliveras ARubio A(2019)Incomplete SMT Techniques for Solving Non-Linear Formulas over the IntegersACM Transactions on Computational Logic10.1145/334092320:4(1-36)Online publication date: 17-Aug-2019
https://dl.acm.org/doi/10.1145/3340923
Xie XChen BZou LLin SLiu YLi XBodden ESchäfer WDeursen AZisman A(2017)Loopster: static loop termination analysisProceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering10.1145/3106237.3106260(84-94)Online publication date: 21-Aug-2017
https://dl.acm.org/doi/10.1145/3106237.3106260
Chen HFlur SMukhopadhyay S(2015)Termination proofs for linear simple loopsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-013-0288-817:1(47-57)Online publication date: 1-Feb-2015
https://dl.acm.org/doi/10.1007/s10009-013-0288-8
Show More Cited By

Recommendations

Termination and invariance analysis of loops
ATVA'05: Proceedings of the Third international conference on Automated Technology for Verification and Analysis

Deductive verification aims to prove deep properties about programs. The classic Floyd-Hoare-style approach to verifying sequential programs reduces program validity queries to first-order validity queries via verification conditions. Proving that a ...
Proving Program Termination by Discoverer and Complete Discrimination System
ISISE '12: Proceedings of the 2012 Fourth International Symposium on Information Science and Engineering

Combined with the tools DISCOVERER and CDS, a method is presented to synthesize ranking functions of loop programs. It is shown that the problems of finding ranking functions can be converted to a simpler problem, which can be solved by the complete ...
Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs
SAS'10: Proceedings of the 17th international conference on Static analysis

Proving the termination of a flowchart program can be done by exhibiting a ranking function, i.e., a function from the program states to a well-founded set, which strictly decreases at each program step. A standard method to automatically generate such ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

CAV '02: Proceedings of the 14th International Conference on Computer Aided Verification

July 2002

629 pages

ISBN:3540439978

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 27 July 2002

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

51
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 30 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Borralleras CLarraz DRodríguez-Carbonell EOliveras ARubio A(2019)Incomplete SMT Techniques for Solving Non-Linear Formulas over the IntegersACM Transactions on Computational Logic10.1145/334092320:4(1-36)Online publication date: 17-Aug-2019
https://dl.acm.org/doi/10.1145/3340923
Xie XChen BZou LLin SLiu YLi XBodden ESchäfer WDeursen AZisman A(2017)Loopster: static loop termination analysisProceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering10.1145/3106237.3106260(84-94)Online publication date: 21-Aug-2017
https://dl.acm.org/doi/10.1145/3106237.3106260
Chen HFlur SMukhopadhyay S(2015)Termination proofs for linear simple loopsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-013-0288-817:1(47-57)Online publication date: 1-Feb-2015
https://dl.acm.org/doi/10.1007/s10009-013-0288-8
Li YZhi LWatt S(2014)A recursive decision method for termination of linear programsProceedings of the 2014 Symposium on Symbolic-Numeric Computation10.1145/2631948.2631966(97-106)Online publication date: 28-Jul-2014
https://dl.acm.org/doi/10.1145/2631948.2631966
Ben-Amram AGenaim S(2014)Ranking Functions for Linear-Constraint LoopsJournal of the ACM10.1145/262948861:4(1-55)Online publication date: 1-Jul-2014
https://dl.acm.org/doi/10.1145/2629488
Larraz DNimkar KOliveras ARodríguez-Carbonell ERubio A(2014)Proving Non-termination Using Max-SMTProceedings of the 16th International Conference on Computer Aided Verification - Volume 855910.1007/978-3-319-08867-9_52(779-796)Online publication date: 18-Jul-2014
https://dl.acm.org/doi/10.1007/978-3-319-08867-9_52
Ghardallou WGlinz MMurphy GPezzè M(2012)Using invariant relations in the termination analysis of while loopsProceedings of the 34th International Conference on Software Engineering10.5555/2337223.2337471(1519-1522)Online publication date: 2-Jun-2012
https://dl.acm.org/doi/10.5555/2337223.2337471
Kling MMisailovic SCarbin MRinard M(2012)BoltACM SIGPLAN Notices10.1145/2398857.238464847:10(431-450)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2398857.2384648
Kling MMisailovic SCarbin MRinard MLeavens GDwyer M(2012)BoltProceedings of the ACM international conference on Object oriented programming systems languages and applications10.1145/2384616.2384648(431-450)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2384616.2384648
Chen HFlur SMukhopadhyay S(2012)Termination proofs for linear simple loopsProceedings of the 19th international conference on Static Analysis10.1007/978-3-642-33125-1_28(422-438)Online publication date: 11-Sep-2012
https://dl.acm.org/doi/10.1007/978-3-642-33125-1_28
Show More Cited By

View Options

View options

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 Publication

Media

Figures

Other

Tables

View Table of Contents