Hubert Garavel

Address: INRIA Grenoble Rhône-Alpes
655, avenue de l'Europe
F-38330 Montbonnot Saint-Martin
Phone: +(33) 4 76 61 52 24
Fax: +(33) 4 76 61 52 52

Current Position

Directeur de Recherche INRIA
Member of the CONVECS team (INRIA Grenoble Rhône-Alpes and LIG)
Invited scientist at Saarland University

Research Interests

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.

Version 3.26 - Date 2015/09/09 11:44:05