IMITATOR − Parameter synthesis for real-time systems

IMITATOR is a software tool for parametric verification and robustness analysis of real-time systems with parameters. It relies on the formalism of networks of parametric timed automata, augmented with integer variables and stopwatches.

IMITATOR implements the following algorithms:

Its extension to stopwatches (since IMITATOR 2.5) with clock updates allow its use in the framework of robust and parametric scheduling analysis of preemptive real-time systems [AFKS12].

IMITATOR is fully written in OCaml, and makes use of the Parma Polyhedra Library. It is available under the GNU General Public License.


IMITATOR implements the following features:

Examples of graphical outputs

Trace set PTA export Trace set Behavioral cartography

The Team

IMITATOR has been initiated, and is still mainly developed, by Étienne André.

The following people contributed to IMITATOR.

Étienne André (2008– )
Camille Coti (2014)
Daphne Dussaud (2010)
Sami Evangelista (2014)
Ulrich Kühne (2010–2011)
Nguyễn Hoàng Gia (2014– )
Romain Soulat (2010–2013)
Compiling and packaging
Corentin Guillevic (2015)
Sarah Hadbi (2015)
Fabrice Kordon (2015)
Alban Linard (2014–2015)
Moral support and suggestions by
Emmanuelle Encrenaz
Laurent Fribourg
Giuseppe Lipari


IMITATOR’s logo (the monkey on top of each page!) is a modifier version of KaterBegemot's Typing monkey.svg. Licence: Creative Commons Attribution-Share Alike 3.0 Unported.


IMITATOR got support from the following institutions and projects.

Conferences on formal methods

Our list of conferences on formal methods