Sciweavers

Share
CADE
2008
Springer

Aligator: A Mathematica Package for Invariant Generation (System Description)

8 years 4 months ago
Aligator: A Mathematica Package for Invariant Generation (System Description)
We describe the new software package Aligator for automatically inferring polynomial loop invariants. The package combines algorithms from symbolic summation and polynomial algebra with computational logic, and is applicable to the rich class of P-solvable loops. Aligator contains routines for checking the P-solvability of loops, transforming them into a system of recurrence equations, solving recurrences and deriving closed forms of loop variables, computing the ideal of polynomial invariants by variable elimination, invariant filtering and completeness check of the resulting set of invariants.
Laura Kovács
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where CADE
Authors Laura Kovács
Comments (0)
books