Proving Termination of Nonlinear Command Sequences
[PDF] [PS] [PS.BZ2] [VIEW]
Bibtex:
@article{babic12termination,
author = {Domagoj Babi\'c and Byron Cook and Alan J.~Hu and Zvonimir Rakamari\'c},
title = {{Proving Termination of Nonlinear Command Sequences}},
journal = {Formal Aspects of Computing},
publisher = {Springer},
pages = {1--15},
url = {http://dx.doi.org/10.1007/s00165-012-0252-5},
year = {2012},
}
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.