Main Software Contributions of Frédéric LANG

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

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:

	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

FLAC

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

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

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.