
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, 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)}, publisher = {Springer}, volume = {25}, number = {3}, pages = {389--403}, month = {May}, year = {2012} }