ALICe documentation

ALICe – A Benchmark for Automatic Loop Invariant Computation

Contents   ::   List of models  »

ALICe – A Benchmark for Automatic Loop Invariant Computation

ALICe project aims to provide tools and a standardized set of test cases to compare different polyhedral analysis techniques and softwares. Currently, ALICe is able to run Aspic and PIPS and with various analysis configurations.

Test cases

Test cases are small-sized, yet non-trivial examples taken from previously published articles, including work by Gonnord, Gulwani, Halbwachs, Jeannet & al. Common models, such as subway or car transition systems, are present.

Installing ALICe

Getting it

Clone the git repository:

git clone


ALICe relies on several softwares, each comes with dependencies. On Debian/Ubuntu, install the following packages:

sudo apt-get install autoconf libtool git svn cproto flex bison libreadline-dev

Then run the script at the root of the git repository to compile and install the required programs:

./ [-jN]

If everything goes well, just setup the environment:


and then you are ready to use ALICe.


Fsmtools is free software, licensed under the GPLv3 license.

Contents   ::   List of models  »