Sciweavers

Share
CSR
2008
Springer

Invariant Generation for P-Solvable Loops with Assignments

9 years 1 months ago
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.
Laura Kovács
Added 19 Oct 2010
Updated 19 Oct 2010
Type Conference
Year 2008
Where CSR
Authors Laura Kovács
Comments (0)
books