The ALIGATORS Tool

Short Description

Aligators is a Mathematica package for inferring quantified invariants of loops iterating over mult-dimensional arrays, such as matrices. When used on matrices, matrix shapes as type invariants (upper-triangular, diagonal, etc) can be derived from the invariant inferred by Aligators.

Aligators is a generalization of the Aligator package.

Inputs to Aligators are nested for-loops iterating iterating linearly (row-by-row or column-by column) over the matrix content by incrementing (or decrementing) the matrix row and column indices, and with assignments, sequencing, and nested conditionals over scalar and matrix variables in the innermost loop body.

We require that the innermost loop body fulfills the conditions below:

it only contains assignments to variables and nested conditionals;
scalar variables in assignments range over integers;
assignments over matrices involve initializations, uninterpreted function symbols, and copies from other matrices;
scalar variables can be expressed as polynomials of the initial values of variables, the loop counter, and some new variables, where there are algebraic dependencies among the new variables;
conditional tests are polynomial relations of degree 1 or 2 in both matrix indeces;
conditional tests are pairwise mutually exclusive;
disjunction of conditional tests is a valid formula.

Aligators was implemented in Mathematica. It

linearizes matrices into one-dimensional (1D) arrays;
rewrites nested loops iterating over matrices with conditional updates into an equivalent sequence of unnested loops over 1D arrays without conditionals using symbolic summation and constraint solving;
derives numeric and quantified invariants for each unnested loop using symbolic summation in the theory of scalars, arrays, and uninterpreted function symbols;
generates quantified invariants over matrices from which matrix type invariants can be proved or proved.

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 Aligators.m of

Aligators.tar.gz (encoded)

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

If you do not have Mathematica installed, you might study the demo file Demo.pdf.

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:

T. A. Henzinger, T. Hottelier and L. Kovács (2009), Type Invariants for Matrices Technical Report, EPFL, Switzerland. [pdf]

Versions and Bugs

The tool was written and developed at at MTC, EPFL, Switzerland.

Right now you are using Version 0.3, last updated on January 29, 2009.

Please report any bugs and comments to Laura Kovács.