Ecole Polytechnique Fédérale de Lausanne
Aligators Tool
english only


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:

Aligators was implemented in Mathematica. It

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.

Copyright © 2009 Laura Kovács — all rights reserved. Commercial use of the software is prohibited without prior written permission.

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

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.


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.