CADP
Since July 2000, I have been working in the VASY (until December 2011), then CONVECS (until 2026), and finally ARMADHA teams of INRIA, Centre de l'Université Grenoble Alpes. I have been contributing to the development of the following software tools:
|
CADP
|
CADP is a software toolbox for the validation and verification of asynchronous concurrent systems. I am one out of the four main authors of CADP, together with Hubert Garavel, Radu Mateescu, and Wendelin Serwe.
We received two scientific prizes for our work on CADP:
Besides participating to maintenance, debugging, and documentation, I am the main developper of the following CADP software tools:
|
BCG_MIN 2.0 / BCG_CMP 1.0: minimisation / comparison of explicit state graphs (including Markovian models) modulo various equivalence relations |
|
|
EXP.OPEN 2.0: compilation of networks of automata into the OPEN/CAESAR environment |
|
|
PROJECTOR 3.0: on-the-fly state graph generation under environment constraints |
|
|
REDUCTOR 5.0: on-the-fly state graph reduction modulo various equivalence relations |
|
|
SVL 2.0: compilation of compositional verification scripts into Bourne shell scripts |
In addition, I have been contributing actively to the development of the following software tools:
|
|
BCG: an environment for handling explicit state graphs |
|
|
FSP2LOTOS / FSP.OPEN: translation of the FSP language of Kramer & Magee (Imperial College, London) to LOTOS and networks of automata |
|
|
LNT2LOTOS / LNT.OPEN: translation of the LNT (formerly known as LOTOS NT) language to LOTOS |
|
|
TRAIAN 3.0: LNT static semantics and compilation of LNT types and functions to the C language |
|
PMC
|
PMC is a prototype partial model checker for EXP.OPEN networks of communicating automata and MCL temporal logic formulas, which is built on top of CADP but is distributed independently. I am the main developer of this tool, parts of which were developed by Radu Mateescu.
|
FLAC
|