Proving Termination of Nonlinear Command Sequences

Share

Domagoj Babic, Byron Cook, Alan J. Hu, Zvonimir Rakamaric. Formal Aspects of Computing (FAC), 2012. (Invited.)
[pdf] [bib]

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.

Bibtex:

@article{fac2012-bchr,
  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 (FAC)},
  volume = {25},
  number = {3},
  year = {2013},
  month = {May},
  pages = {389--403},
  publisher = {Springer}
}