Kovacs, Laura2010-11-302010-11-302010-11-30200810.1007/978-3-540-78800-3_18https://infoscience.epfl.ch/handle/20.500.14299/61480WOS:000254735100018We present a method for generating polynomial invariants for a subfamily of imperative loops operating on numbers, called the P-solvable loops. The method uses algorithmic combinatorics and algebraic techniques. The approach is shown to be complete for some special cases. By completeness we mean that it generates a set of polynomial invariants from which, under additional assumptions, any polynomial invariant can be derived. These techniques are implemented in a new software package Aligator written in Mathematica and successfully tried on many programs implementing interesting algorithms working on numbers.Identitiestext::conference output::conference proceedings::conference paper