非线性循环不变式的自动生成

提出了一个自动生成非线性循环不变式的算法。循环不变式可以表示成一个带参数的多项式的形式，根据断言的归纳特性，将循环不变式的生成问题转变成一个约束求解问题，这个约束求解问题的每个解对应于一个循环不变式，如果约束求解问题仅有零解，则说明不存在该参数多项式形式的循环不变式。该算法在Maple中得到了实现，并通过一些实例说明了该算法的有效性。

Automatic generation of non-linear loop invariants

This paper proposed an approach to automatically generate non-linear loop invariants. An invariant of a loop was hypothesized as a parameterized polynomial. Based on the inductive assertion's properties, we reduced the non-linear loop invariant problem to a numerical constraint solving problem. All the solutions to these constraints were the non-linear loop invariants of the program. The approach has been implemented in Maple. The implementation has been used to automatically discover nontrivial invariants for many programs.