Our work for invariant generation does neither use abstract interpretation nor
constraint solving, and does not fix an a priori bound on the degree of the
polynomial invariants to be synthesised. Instead, we
restrict the class of loops our work can handle to non-deterministic loops
whose loop updates yield special classes of algebraic recurrences in
the loop counter, and hence we cannot handle loops with arbitrary
nestedness as in [1]}.
We rely on results of [2]} proving that the set of all polynomial equality
invariants for a given (non-deterministic) loop forms a polynomial
ideal. In [3]}, we use the ideal-theoretic
result of [2]} and compute all polynomial
invariants of the class of non-deterministic
loops that can be modelled by
C-finite recurrence equations. Our results can further be extended to
more complex recurrences equations by allowing restricted
multiplications, and hence restricted classes of linear recurrences
with polynomial coefficients, among loop variables - as detailed
in [5]}, [6]}.
