Proving termination of nonlinear command sequences
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 condition. The analysis allows us to automatically prove the termination of loops that cannot be handled using previous techniques. We also describe a method for integrating our nonlinear termination proving technique into a larger termination proving framework that depends on linear reasoning.
nonlinear assignments divergence testing program termination well-foundedness provers