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.


Published in:
Automated Reasoning, Proceedings, 5195, 275-282
Presented at:
4th International Joint Conference on Automated Reasoning, Sydney, AUSTRALIA, Aug 12-15, 2008
Year:
2008
Publisher:
Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa
ISBN:
978-3-540-71069-1
Keywords:
Laboratories:




 Record created 2010-11-30, last modified 2018-01-28


Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)