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.
Keywords for this software
References in zbMATH (referenced in 8 articles , 1 standard article )
Showing results 1 to 8 of 8.
- Henzinger, Thomas A.; Hottelier, Thibaud; Kovács, Laura; Voronkov, Andrei: Invariant and type inference for matrices (2010)
- Kovács, Adalbert; Kovács, Laura: Deciding properties of affine loops (2010)
- Kovács, Laura: A complete invariant generation approach for P-solvable loops (2010)
- Platzer, André; Quesel, Jan-David; Rümmer, Philipp: Real world verification (2009)
- Armando, Alessandro (ed.); Baumgartner, Peter (ed.); Dowek, Gilles (ed.): Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12--15, 2008 Proceedings (2008)
- Kovács, Laura: Aligator: A Mathematica package for invariant generation. (System description) (2008)
- Kovács, Laura: Invariant generation for P-solvable loops with assignments (2008)
- Kovács, Laura: Reasoning algebraically about P-solvable loops (2008)