Download IMITATOR

Version History

Version	Reachability graph	Inverse Method	Variants of IM	Cartography	Graphical Output	Stopwatches	Arbitrary updates	Correctness patterns
2.6	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes
2.5	Yes	Yes	Yes	Yes	Yes	Yes	Yes	No
2.4	Yes	Yes	Yes	Yes	Yes	Yes	No	No
2.3	Yes	Yes	Yes	Yes	Yes	No	No	No
2.0 to 2.2	Yes	Yes	No	Yes	Yes	No	No	No
1.x	No	Yes	No	No	No	No	No	No

Version 2.6 (released 25.02.2013)
- Addition of observer patterns
Version 2.5 (released 21.08.2012)
- Addition of arbitrary clock updates (instead of resets)
Version 2.4 (released 20.02.2012)
- Extension of the input syntax to stopwatches
- Addition of a state merging technique reducing state space for all algorithms
Version 2.3 (released 09.06.2011)
- Addition of variants of the inverse method algorithm
- Addition of an optional optimization of the inverse method algorithm
- Several optimizations to speed up post image computation
Version 2.2 (released 30.07.2010)
- Several optimizations to speed up post image computation
- More detailed presentation of reachability graph
- Graphical output of behavioral cartography
- Refactoring of source code to improve maintainability
Version 2.1 (released 31.05.2010)
- Replaced Apron by PPL for faster polyhedral operations
Version 2.0 (released 2010)
- Complete reimplementation in OCaml
- Uses Apron library for polyhedral operations
- Implements behavioral cartography
- Generates graphical output of reachability graph
Version 1.0 (released 2008)
- First prototype implementation in Python
- Implements inverse method for PTA
- Calls HyTech to perform post image operation

See changelog for details changes in each version.

Binaries and Sources

Due to the difficulty of installing some libraries needed by IMITATOR (especially PPL), we recommend you download one of the binaries. If you prefer to install the source, please read the installation instructions below.

Latest binaries have been compiled using KUbuntu 12.10, and can be used on all Ubuntu-like systems, e.g., Debian. Older binaries have been compiled using older versions of Ubuntu, and can also be executed on all Ubuntu-like systems.

In case you want to use the graphical output facilities, don’t forget to install dot (from the Graphviz package) and graph (from the plotutils package). This is true even if you download the standalone binaries.

IMITATOR is available under the GNU General Public License.

Version	Release date	Sources	Binary (32 bits)	Binary (64 bits)	User Manual
IMITATOR 2.6.2 (working version)	-	GitHub
IMITATOR 2.6.1 (latest stable version)	01.05.2013	[imitator-2.6.1.tar.gz]	[imitator-2.6.1-bin32.tar.gz]	[imitator-2.6.1-bin64.tar.gz]	[PDF]
IMITATOR 2.6.0	25.02.2013	[imitator-2.6.0.tar.gz]	[imitator-2.6.0-bin32.tar.gz]	[imitator-2.6.0-bin64.tar.gz]	[PDF]
IMITATOR 2.5.0	21.08.2012	[imitator-2.5.0.tar.gz]	[imitator-2.5.0-bin32.tar.gz]	[imitator-2.5.0-bin64.tar.gz]	[PDF]
IMITATOR 2.4	20.02.2012	[imitator-2.4.tar.gz]	[N/A]	[N/A]	[N/A]
IMITATOR 2.3	09.06.2011	[imitator-2.3.tar.gz]	[imitator-2.3-bin.tar.gz]*	[N/A]	[PDF]
IMITATOR 2.2	30.07.2010	[imitator-2.2.tar.gz]	[imitator-2.2-bin.tar.gz]*	[N/A]	[PDF]
IMITATOR 2.1	31.05.2010	[N/A]	[N/A]	[N/A]	[N/A]
IMITATOR 2.0	2010	[N/A]	[N/A]	[N/A]	[N/A]
IMITATOR 1.0	2008	[IMITATOR.py]	[N/A]	[N/A]	[N/A]

* These binaries might not be standalone, depending on your configuration.

Installing IMITATOR from sources

In short, in order to compile IMITATOR from source, you need to install the following libraries and tools. Installing these libraries might entail additional dependencies.

A C++ compiler (package "g++" in Ubuntu)
m4 (package "m4" in Ubuntu)
OCaml
The OCaml ExtLib library (Extended Standard Library for Objective Caml)
The Parma Polyhedra Library (PPL), compiled including the OCaml interface
The GNU Multiprecision Library (GMP) with the OCaml interface
dot, a module of graphviz, required for the graphical output, but not necessary to compile and run IMITATOR

Before compiling IMITATOR from the source code, make sure that all dependencies are met. In the following, we give detailed instructions on how to install the necessary tools and libraries. All these instructions can also be found in the INSTALL.txt file inside the IMITATOR source archive.

We give for each package the version number used for developing IMITATOR.

C++ compiler

Install a C++ compiler using your favorite package manager (package "g++" in Ubuntu).

m4

Install m4 using your favorite package manager (package "m4" in Ubuntu).

OCaml (v 3.12.1)

The Ocaml runtime environment and libraries are usually available as preconfigured packages (package "ocaml" in Ubuntu, coming with numerous dependencies).

Otherwise, get the sources here. Proceed as follows to compile:

> ./configure --prefix=/usr
> make world
> make bootstrap
> make opt
> make opt.opt
> sudo make install

OCaml Extended libraries (v 1.5.2)

Install OCaml Extlib (Extended libraries) using your favorite package manager (packages "libextlib-ocaml" and "libextlib-ocaml-dev" in Ubuntu).

Alternatively, you can download Extlib here. Create a build directory and start the installation:

> mkdir build
> ocaml install.ml

Then, select "both" and the directory "build". After installation, copy the files to your local OCaml directory:

> sudo mkdir /usr/lib/ocaml/extlib
> sudo cp build/* /usr/lib/ocaml/extlib

GNU Multiprecision Library (GMP) (v 10)

Install the GMP library and header with your favorite package manager (package "libgmp" in Ubuntu, usually pre-installed). Don’t forget to add the OCaml binding (this may include at least "libgmp-devel", "libgmp-ocaml" and "libgmp-ocaml-dev").

If everything is fine, skip to the installation of PPL. Otherwise, you will need to compile manually as follows.

First get the sources here and install as follows:

> export CPPFLAGS=-fexceptions
> ./configure --enable-cxx --prefix=/usr
> make
> make check
> sudo make install

Then, install MPFR (3.1.0): get the sources here and install as follows:

> ./configure --prefix=/usr --with-gmp-lib=/usr/lib --with-gmp-include=/usr/include
> make
> make check
> sudo make install

Then install the OCaml interface for the GMP library, get the sources here. Then, open the Makefile in an editor and set the following variables:

GMP_LIBDIR=/usr/lib
GMP_INCLUDES= -I=/usr/include

Then you should be able to compile:

> make
> sudo make install

Parma Polyhedra Library (PPL) (v1.0)

Usually, the OCaml interface is not part of available packages. Thus, get the sources and compile them:

> ./configure --prefix=/usr  
> make
> sudo make install

If all dependencies have been correctly installed (which will be detected by PPL very soon), the installation of PPL is straightforward. However, note that the compiling phase (make) can be very long (up to an hour).

Installing IMITATOR

In order to compile the sources of IMITATOR, some path variables need to be set. You can do this by either editing the Makefile, or by using environment variables within your shell. In the latter case, use the following code to set the respective paths:

> export EXTLIB_PATH=/path/to/ocaml/extlib
> export OCAML_PPL_PATH=/path/to/ppl/ocaml/interface
> export OCAML_GMP_PATH=/path/to/gmp/ocaml/interface
> export CLIB_PATH=/path/to/native/libs

The native libraries needed to compile and link IMITATOR include libgmp.a, libgmpxx.a, libmlgmp.a, libpwl.a and libppl.a. These should be accessible via the CLIB_PATH. The OCaml interface for the GMP library comprises the files gmp.mli, gmp.cmi and gmp.cma. The Ocaml interface of PPL includes ppl_ocaml.mli, ppl_ocaml.cmi and ppl_ocaml.cma. If all these requirements are met, then IMITATOR can be compiled and linked by typing

> make

Case studies

Download the case studies on the case studies page.

Using IMITATOR

Read the user manual for more information.

Contact

In case you meet any problem, please contact us.