Invariant generation for p-solvable loops with assignments

Abstract

We 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. © 2008 Springer-Verlag Berlin Heidelberg.