Conference paper

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.


  • There is no available fulltext. Please contact the lab or the authors.

Related material