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.
Citation
Domagoj Babic,
Byron Cook,
Alan J. Hu,
Zvonimir Rakamaric
Proving Termination of Nonlinear Command Sequences
Formal Aspects of Computing (FAC), 25(3): 389--403, doi:10.1007/s00165-012-0252-5, 2012.
BibTeX
@article{2012_fac_bchr,
title = {Proving Termination of Nonlinear Command Sequences},
author = {Domagoj Babic and Byron Cook and Alan J. Hu and Zvonimir Rakamaric},
journal = {Formal Aspects of Computing (FAC)},
volume = {25},
publisher = {Springer},
pages = {389--403},
doi = {10.1007/s00165-012-0252-5},
number = {3},
month = {may},
year = {2012}
}
Acknowledgements
We would like to thank Richard Fateman, Robert Israel, and Daniel Lichtblau for useful discussions about the complexity of polynomial factorization, divergence of the update functions, and multivariate limits, and Josh Berdine and Jacopo Mantovani for their comments on Section 3. We would also like to thank the anonymous reviewers for many helpful comments and for pointing out the special case in the computation of safe RGDs.