Kovacs, Laura2010-11-302010-11-302010-11-30200810.1007/978-3-540-79709-8_35https://infoscience.epfl.ch/handle/20.500.14299/61343WOS:000256351100035We discuss interesting properties of a general technique for inferring polynomial invariants for a subfamily of imperative loops, called the P-solvable loops, with assignments only. The approach combines algorithmic combinatorics, polynomial algebra and computational logic, and it is implemented in a new software package called Aligator. We present a collection of examples illustrating the power of the framework.IdentitiesProgramtext::conference output::conference proceedings::conference paper