Proving Termination by Divergence
[PDF] [PS] [PS.BZ2] [VIEW]
Bibtex:
@inproceedings{bhrc07termination,
author = {Domagoj Babi\'c and Alan J. Hu and Zvonimir Rakamari\'c
and Byron Cook},
title = {{Proving Termination by Divergence}},
booktitle = {SEFM'07: Proceedings of the 5th IEEE International
Conference on Software Engineering and Formal Methods},
publisher = {IEEE Computer Society},
location = {London, UK},
month = {September},
year = {2007},
pages = {93--102},
}
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.