Invariant Generation for P-Solvable Loops with Assignments

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.

• Type: Conference
• Year: 2008
• Where: CSR
• Authors: Laura Kovács
• Keywords: CSR 2008, Imperative Loops, Package Called Aligator, Polynomial Invariants, Theoretical Computer Science