Aligator: A mathematica package for invariant generation
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.
WOS:000258887400022
2008
978-3-540-71069-1
Lecture Notes In Artificial Intelligence; 5195
275
282
REVIEWED
Event name | Event place | Event date |
Sydney, AUSTRALIA | Aug 12-15, 2008 | |