MeFoSyLoMa CNRS Iniria
QR Code
Last modified
June 28, 2016

Sep 20, 2018
Home Page

What is ?

is a software environment whose goal is the formal specification and verification of dynamic systems.

It has been designed in order to:

This environment consists of two software tools: Coloane, the graphical interface, and Alligator, an integration framework based web services. It is enlarged with the existing verification tools developed in our laboratories (founding members or partners).

Why ?

The development of has been decided and it is supported by three partners of the Parisian verification group, MeFoSyLoMa.

This group is composed of seven teams. and the founding members of are LIP6, LIPN and LSV.

First, these members aim at sharing their tools, comparing and supporting industrial case studies and finally making them long-lasting.

Second, they also want to promote the practice of formal verification in industry and thus they intend to ease the task of integration of new formalisms and tools.


is managed by a steering committee consisting of researchers and engineers. It decides strategic orientations as well as technical choices.

Current Tools

Two formalisms are supported: automata and Petri nets, both with extensions.

Most of the tools are related to Petri nets. Some of them perform structural analyses like invariant computations.

while other tools perform behavioural analyses: symbolic reachability graph building, unfolding, stochastic simulations, etc.

Finally some of them transform high-level nets into low-level ones.

Software Status

All the developed software are open source and free software tools.

Alligator is published under the GNU Affero General Public License (AGPL) version 3 .

Coloane is published under the Eclipse Public License (EPL) version 1 .