Proving Termination by Divergence

We describe a novel and efficient algorithm for proving the termination 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 known techniques. The paper closes with experimental results using examples drawn from industrial code