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 rational-valued global variables, stopwatches, multi-rate clocks, and some other useful features.

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-…)
Vincent Bloemen (2018)
Jaime Arias (2018-…)
Camille Coti (2014)
Daphne Dussaud (2010)
Sami Evangelista (2014)
Ulrich Kühne (2010-2011)
Nguyễn Hoàng Gia (2014-2017)
Laure Petrucci (2019-…)
Jaco van de Pol (2019-…)
Romain Soulat (2010-2013)
Compiling, packaging and external tools
Jaime Arias (2018-…)
Corentin Guillevic (2015)
Sarah Hadbi (2015)
Jawher Jerray (2018-2019)
Fabrice Kordon (2015)
Alban Linard (2014-2015)
Sahar Mhiri (2018)
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