Proving Termination by Divergence

Domagoj Babic, Byron Cook, Alan J. Hu, Zvonimir Rakamaric. 5th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), London, UK.
[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 termination condition. The analysis allows us to automatically prove the termination of loops that cannot be handled using previous techniques. The paper closes with experimental results using short examples drawn from industrial code.

Bibtex:

@inproceedings{sefm2007-bchr,
  author = {Domagoj Babi\'c and Byron Cook and Alan J. Hu and
    Zvonimir Rakamari\'c},
  title = {Proving Termination by Divergence},
  booktitle = {Proceedings of the 5th IEEE International Conference on
    Software Engineering and Formal Methods (SEFM 2007)},
  publisher = {IEEE Computer Society},
  year = {2007},
  pages = {93--102},
}