Omega IST projet (2002-2004) «Correct Development of Real-Time Embedded Systems » in collaboration with France Telecom and EADS Space.
Expresso RNTL projet (2001-2003) « Real-time JAVA for embedded systems» in collaboration with SILICOMP, Aonix and IRISA.
Taxys RNRT projet (1999-2001) : Analysis of synchronous embedded software for cellular phones, in collaboration with Alcatel Business Systems et France Télécom.
Proust RNRT project (1998-2000): Definition of a timed extension for the SDL international standard of ITU.
DDV project (1993-1995) : Evaluation of formal techniques on a fault-tolerant architecture, ESA/ESTEC, in collaboration with Matra-Marconi-Space and Dornier.
VIRES project (1996-1999): Verifying Industrial Reactive Systems, European Long Term Research Project.
REACT project (1993-95): Building Correct Reactive Systems, European Long Term Research Project.
Spec project (1990-92): Formal Methods and Tools for the Development of Distributed and Real-Time Systems, European Basic Research Project.
TGV project (1994-95).: Joint Verilog-Verimag-Irisa project for the development of a test case generation tool from test purposes and SDL models of communication protocols.
Caesar project and the CADP toolset (1989-92) : Development of a compiler/model checker for the LOTOS language by H. Garavel. The CADP integrates Caesar and a set of static analysis and verification tools.
Vesar project (1988-90): Development of an environment integrating Xesar and the test case generator VEDA of France Telecom, in collaboration with Verilog SA.
Xesar project (1985-87): Development under France Telecom contract of a model-checker for the Estelle ISO standard for communication protocols. Xesar has been succesfully used in the Esprit Delta-4 project for the validation of a fault-tolerant token-ri,ng protiocol in collaboration with Bull and Laas (1988-90).