The ALIGATOR Tool

Short Description

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

for loops with assignments only,
and, under additional assumptions, for loops with assignments and nested conditionals.

The Aligator package contains routines for

checking the P-solvability of a loop,
transforming loops into a system of recurrence equations,
solving recurrences and deriving closed forms of loop variables,
merging closed form systems of loop sequences,
computing the ideal of polynomial invariants by variable elimination and invariant filtering (if necessary).

New version of Aligator for generating quantified invariants over multi-dimensional arrays is available from here.

Registration and Legal Notices

The source code for this package is password protected. To get the password send an email to Laura Kovács. It will be given for free to all researchers and non-commercial users.

A Note on Encoded Files

The package is encoded. It cannot be read or modified directly as plain text, but can be loaded into Mathematica just like any normal input file (i.e., with <<"file" or Get["file"]). There is no need (and also no way) to decode them by using additional software or a special key.

If loading an encoded file causes a syntax error, open it with a text editor and remove any blank lines at the beginning.

The Package

The package is contained in the Mathematica input file Aligator.m of

Aligator.tar.gz (encoded)

and is accompanied by the Mathematica notebooks

Demo.nb and Inside Aligator.nb

It is developed for Mathematica 5.2 and might not run properly on earlier and/or later versions.

For some experimental results of Aligator see AligatorDemoTimings.nb and TextbooksExperiments.pdf.

If you do not have Mathematica installed, you might study the pdf versions Demo.pdf, Inside Aligator.pdf and AligatorDemoTimings.pdf of the demo files.

Literature

To use the implementation it is sufficient to study the demo files above. It contains many examples to start with.

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])

Versions and Bugs

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.

Aligator in Software Verification

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.