Hubert Garavel - Home Page

![]() |
|

|
|
|
|

|
|
My main research interest is about the application of formal methods to the development of complex systems, whatever their nature (hardware, software, or telecom). Although I can appreciate the theoretical beauties of some mathematical approaches, I pay attention to practical applicability and I am mostly interested in formal methods at work . In the past, I worked on various formal techniques, including ESTELLE (for which I designed a compiler and a simulation/verification tool named VEDA-2, which has been later reused by Verilog to bring verification capabilities in the Geode tool for SDL) and the synchronous dataflow language LUSTRE (for which I designed the compiler and C code generator used in Verilog's SAGA/SAO+ workbench). However, process algebras seem to be the appropriate formalism for specifying and verifying complex, distributed systems in a clean and effective way. As far as practical applications are concerned, I mostly work with LOTOS, which (in spite of its bizarre syntax) presents the double advantage of being an international standard and providing sufficient expressiveness for real-life applications. My main piece of software is CADP (Construction and Analysis of Distributed Processes), an advanced protocol engineering toolbox. This is a team work, in which I manage the LOTOS-related aspects (including the CAESAR and CAESAR.ADT compilers) as well as support for enumerative and "on the fly" verification (namely the BCG and OPEN/CAESAR environments). I am involved in several industrial projects in which LOTOS and CADP are applied to the formal specification and verification of safety-critical systems. |
|
| |
|
| |
|
|

|
|
|
|

