The works of [1]} and [2]} fix a
polynomial template invariant and derive a constraint problem that encodes
properties of loop invariants, such as inductiveness. These constraint problems
are then solved by linear or polynomial algebra.
The methods of [3]} and [4]}
use abstract interpretation in combination with Gröbner bases computations for
computing polynomial invariants of bounded
degree. In [5]}, the abstract interpretation approach from [3]} and the
constraint-based approach from [1]} is
combined, yielding a
procedure for computing invariants of bounded degree without resorting to
Gröbner bases.
