Since July 2000, I have been working in the VASY (until December 2011) then CONVECS (since January 2012) teams of INRIA Grenoble Rhône-Alpes. I have been contributing to the development of the following software tools:
CADP is a tool box for the validation and verification of asynchronous systems. I participate actively to maintenance, debugging, and documentation. I am also the main developper of the following software tools:
|BCG_MIN 2.0 / BCG_CMP 1.0: minimisation / comparison of explicit state graphs (including Markovian models) modulo various equivalences|
|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 contribute to the development of the following software tools:
FLAC is a translator from FIACRE 2.0 to LOTOS, for verification using CADP. I try to maintain this open-source tool, mostly developed in SML by Xavier Clerc when he was an engineer in the VASY team, upon an algorithm that I devised.
PMC is a partial model checker for EXP.OPEN networks of communicating automata and MCL temporal logic formulas. I am the main developer of this tool, parts of which were developed by Radu Mateescu.
TRAIAN is a compiler for LOTOS NT (an old version of LNT) data types. I actively contribute to the development of version 3 of TRAIAN, together with Hubert Garavel and Wendelin Serwe.