|
My main research interest is about formal methods at work, namely the application of formal methods to the development of critical systems of all kinds (hardware, software, or telecom). I appreciate the theoretical beauties of mathematical approaches, but I also pay attention to practical applicability issues.
In the past, I worked on various formal techniques, such as ESTELLE, a protocol description language for which I designed a compiler and a simulation/verification tool named VEDA-2 that later inspired the ObjectGeode tool for SDL, and LUSTRE, a synchronous dataflow language for which I designed the compiler and C code generator of the SAGA/SAO+/SCADE workbench used to produce avionics, nuclear, and transportation embedded software.
To specify and verify large concurrent systems in a rigorous and effective way, process calculi provide the most appropriate semantical foundations. For many years, I have been working on the implementation of LOTOS, an international standard that combines the best features of Hoare's CSP and Milner's CCS, and provides sufficient expressiveness for many applications. I also contributed to the design of the E-LOTOS standard (1993-2001) and, more recently, to the design and implementation of LOTOS NT, a promising language merging functional languages and process calculi.
My main piece of software is CADP (Construction and Analysis of Distributed Processes), an advanced verification toolbox for which I have been the architect and a key developer. Initiated in the 80s, CADP has grown progressively due to a sustained collaborative effort, and now contains more than fifty different tools.
I am currently working on next-generation formal methods that merge concurrency theory with more traditional branches of computer science and provide support for probabilistic, stochastic, and timed aspects.
|
Current Position