Aligator is a Mathematica package for reasoning algebraically about a rich class of imperative loops, called the P-solvable loops. These loops are with assignments, sequencing and conditionals, test conditions are ignored, they work on number and have polynomial closed forms.
Aligator stands for automated loop invariant generation by algebraic techniques over the rationals. It combines symbolic summation and polynomial algebra with computational logic, and automatically generates a finite set of polynomial invariants. The method is shown to be complete - the returned set of polynomials forms a basis of the polynomial invariant ideal
The Aligator package contains routines for
New version of Aligator for generating quantified invariants over multi-dimensional arrays is available from here.
Copyright © 2008 Laura Kovács — all rights reserved. Commercial use of the software is prohibited without prior written permission.
If loading an encoded file causes a syntax error, open it with a text editor and remove any blank lines at the beginning.
Further information can be found here:
L. Kovács (2007), Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema. Ph.D. Thesis, RISC-Linz, Austria. [pdf]
L. Kovács (2008), Reasoning Algebraically About P-solvable Loops. Proc. of TACAS 2008, LNCS 4963, pp. 249-264. (preprint [pdf])
The package was originally written at RISC-Linz, Austria, and developed further at MTC, EPFL, Switzerland.
Right now you are using Version 0.4, last updated on March 30, 2008.
Please report any bugs and comments to Laura Kovács.
An automatic verification tool named
Valigator is now available,
supporting the entire process of imperative program verification:
generating and proving verification conditions, with built-in invariant and
bound assertion inference using Aligator.
To download and use Valigator, click here.