Abstract
We describe a simple and efficient algorithm for proving the termination of a class of loops with nonlinear assignments to variables. The method is based on divergence testing for each variable in the cone-of-influence of the loop’s condition. The analysis allows us to automatically prove the termination of loops that cannot be handled using previous techniques. We also describe a method for integrating our nonlinear termination proving technique into a larger termination proving framework that depends on linear reasoning.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Bouajjani A, Bozga M, Habermehl P, Iosif R, Moro P, Vojnar T (2006) Programs with lists are counter automata. In: Proceedings of international conference on computer aided verification (CAV). pp 517–531
Berdine J, Chawdhary A, Cook B, Distefano D, O’Hearn P (2007) Variance analyses from invariance analyses. In: Proceedings of ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL). pp 211–224
Babić D, Cook B, Hu AJ, Rakamarić Z (2007) Proving termination by divergence. In: Proceedings of IEEE international conference on software engineering and formal methods (SEFM). pp 93–102
Bradley A, Manna Z, Sipma H (2005) Termination of polynomial programs. In: Proceedings of international conference on verification, model checking, and abstract interpretation (VMCAI). pp 113–129
Bradley AR, Manna Z, Sipma HB (2005) The polyranking principle. In: Proceedings of international colloquium on automata, languages and programming (ICALP). pp 1349–1361
Bradley AR, Manna Z, Sipma HB (2005) Termination analysis of integer linear loops. In: Proceedings of international conference on concurrency theory (CONCUR). pp 488–502
Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL). pp 238–252
Cytron R, Ferrante J, Rosen BK, Wegman MN, Zadeck FK (1991) Efficiently computing static single assignment form and the control dependence graph. ACM Trans Prog Lang Syst 13(4): 451–490
Contejean E, Marché C, Monate B, Urbain X (2003) Proving termination of rewriting with cime. In: Extended abstracts of the sixth international workshop on termination (WST). pp 71–73
Cousot P (2005) Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Proceedings of international conference on verification, model checking, and abstract interpretation (VMCAI). pp 1–24
Cook B, Podelski A, Rybalchenko A (2005) Abstraction refinement for termination. In: Proceedings of international static analysis symposium (SAS). pp 87–101
Cook B, Podelski A, Rybalchenko A (2006) Termination proofs for systems code. In: Proceedings of ACM SIGPLAN conference on programming language design and implementation (PLDI). pp 415–426
Colón M, Sipma H (2002) Practical methods for proving program termination. In: Proceedings of international conference on computer aided verification (CAV). pp 442–454
Codish M, Taboch C (1999) A semantic basis for the termination analysis of logic programs. J Logic Prog 41(1): 103–123
Dugundji J, Granas A (2003) Fixed point theory. 1st edn. Springer, New York
Robert W. Floyd (1967) Assigning meanings to programs. In: Mathematical Aspects of Computer Science, vol 19 of Proceedings of Symposia in Applied Mathematics, pages 19–32 American Mathematical Society
Giesl J, Thiemann R, Schneider-Kamp P, Falke S (2004) Automated termination proofs with AProVE. In: Proceedings of international conference on rewriting techniques and applications (RTA). pp 210–220
Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10): 576–583
Kaltofen E (1982) On the complexity of factoring polynomials with integer coefficients. PhD thesis, Rensselaer Polytechnic Institute, Troy, NY, USA
Lenstra AK, Lenstra HW Jr, Lovász L (1982) Factoring polynomials with rational coefficients. Math Ann 261: 515–534
Lee CS, Jones ND, Ben-Amram AM (2001) The size-change principle for program termination. In: Proceedings of ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL). pp 81–92
Lindenstrauss N, Sagiv Y, Serebrenik A (1997) TermiLog. A system for checking termination of queries to logic programs. In: Proceedings of international conference on computer aided verification (CAV). pp 444–447
Maplesoft (2004) Maple, version 9.5
Magill S, Berdine J, Clarke E, Cook B (2007) Arithmetic strengthening for shape analysis. In: Proceedings of international static analysis symposium (SAS)
Muchnick SS (1997) Advanced Compiler Design and Implementation. Morgan Kaufmann Publishers Inc., San Francisco
Podelski A, Rybalchenko A (2004) A complete method for the synthesis of linear ranking functions. In: Proceedings of international conference on verification, model checking, and abstract interpretation (VMCAI). pp 239–251
Chris Speirs, Zoltan Somogyi, Harald Søndergaard (1997) Termination analysis for Mercury. In International Static Analysis Symposium (SAS), pages 160–171
Tip F. (1995) A survey of program slicing techniques. Journal of programming languages 3: 121–189
Tiwari A (2004) Termination of linear programs. In: Proceedings of the international conference on computer aided verification (CAV). pp 70–82
Turing A (1949) Checking a large routine. In: Report of a conference on high speed automatic calculating machines. pp 67–69
Author information
Authors and Affiliations
Corresponding author
Additional information
Jonathan Bowen and Michael Butler
Rights and permissions
About this article
Cite this article
Babić, D., Cook, B., Hu, A.J. et al. Proving termination of nonlinear command sequences. Form Asp Comp 25, 389–403 (2013). https://doi.org/10.1007/s00165-012-0252-5
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-012-0252-5