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.
Citation
Domagoj Babic,
Byron Cook,
Alan J. Hu,
Zvonimir Rakamaric
Proving Termination by Divergence
Proceedings of the 5th IEEE International Conference on Software Engineering and Formal Methods (SEFM), 93--102, doi:10.1109/SEFM.2007.32, 2007.
Invited for special section submission to Formal Aspects of Computing (FAC)
BibTeX
@inproceedings{2007_sefm_bchr,
title = {Proving Termination by Divergence},
author = {Domagoj Babic and Byron Cook and Alan J. Hu and Zvonimir Rakamaric},
booktitle = {Proceedings of the 5th IEEE International Conference on Software Engineering and Formal Methods (SEFM)},
publisher = {IEEE Computer Society},
pages = {93--102},
doi = {10.1109/SEFM.2007.32},
year = {2007}
}
Acknowledgements
We would like to thank Richard Fateman, Robert Israel, and Daniel Lichtblau for useful discussions about the complexity of polynomial factorization, divergence of the update functions, and multivariate limits. We would also like to thank the anonymous reviewers for several helpful comments and for pointing out the special case in the computation of safe RGDs. This work was supported by an NSERC Discovery Grant, a Microsoft Graduate Fellowship, and a graduate fellowship from the University of British Columbia.