Professor at the University Joseph Fourier.and CEA-Leti ("En Délégation" : 2010-11 et 2011-12).
Distributed and Complex Systems group, Verimag Laboratory
Phone : (+33) 04 56 52 03 71
Mailing adress : VERIMAG Centre Équation - 2, avenue de Vignate 38610 GIÈRES
My interests are in the study of embedded systems, formal specification and verification, algorithmic verification techniques, complex systems, real-time systems, automata and logics. My work has been on the topic of automatic formal verification of systems that have unbounded numbers of states. I have pioneered development of techniques that combine the complementary strengths of deductive and algorithmic methods. I have made significant research contributions on several aspects of this problem. I developed the theory of property-preserving abstraction and relationship to compositional verification, automatic invariant discovery, predicate abstraction and a verification method for parametrized systems. All these techniques are employed in the tool InVeSt developed in collaboration with Yassine Lakhnech and Sam Owre from the SRI. Currently, I collaborate with Joseph Sifakis (Turing Award 2007) on the research project "Rigorous Embedded Systems Design - BIP framework". This research project addresses the end-to-end design for large-scale heterogeneous embedded systems. The key motivations are facilitation of the design of advanced heterogeneous embedded systems with distributed SW. At the same time it can provide a rigorous design flow with performance analysis & validation for multiple programming models to target hardware architectures including multiple heterogeneous smart subsystems and components. The aim of the project is to provide a design flows with the following key objectives: