The Community for Technology Leaders
Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05) (2007)
London, England
Sept. 10, 2007 to Sept. 14, 2007
ISBN: 0-7695-2884-8
pp: 93-102
Domagoj Babic , University of British Columbia
Zvonimir Rakamaric , University of British Columbia
Alan J. Hu , University of British Columbia
Byron Cook , Microsoft Research
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.
INDEX TERMS
null
CITATION
Domagoj Babic, Zvonimir Rakamaric, Alan J. Hu, Byron Cook, "Proving Termination by Divergence.", Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), vol. 00, no. , pp. 93-102, 2007, doi:10.1109/SEFM.2007.32
58 ms
(Ver )