Pubs / Proving Termination of Nonlinear Command Sequences

Proving Termination of Nonlinear Command Sequences

[PDF] [PS] [PS.BZ2] [VIEW]

  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 = {},
  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.

Page last modified on August 24, 2012, at 03:53 PM