Model Checking and Verification of Transition Systems
First Results  1982
The first results about “property verification by evaluation of formulas” are in my thesis (Thèse d’Etat) presented in June 1979. These results have been published in the paper “A Unified Approach for Studying the Properties of Transition Systems”  Theoretical Computer Science, Vol. 18, 1992. They include a fixpoint characterization of a simple logic with two modalities: possible and inevitable.
The results of my thesis have also been the basis for work with JP Queille which led to the development of the first model checker CESAR, in 1982. See the related publication. The tool allows translation of finite state CSP programs into Petri nets, extended with finitevalued variables. The verification method is symbolic, representing sets of model states as boolean expressions.
I also published a paper with JP Queille on “A Temporal Logic to Deal with Fairness in Transition Systems” in FOCS 1982, which uses a branching time temporal logic with an until operator to express fairness properties.
Tools for Modelchecking and Testing
– 1982today
The above results are the basis for subsequent work with H. Garavel, S. Graf, JC Fernandez, L. Mounier and M. Bozga, for the development model checking tools for the verification of distributed systems, by enumerative techniques.
These led to three widelydistributed and used verification environments:
 CADP
A tool for the construction and analysis of distributed processes developed by H. Garavel at INRIA.
See the related publication.

IF toolbox
A validation environment for componentbased realtime systems, developed at Verimag.
 TGV
An automatic test case generator for communication protocols, integrated in the ObjectGeode tool commercialized by Telelogic.
Combining modelchecking and model reduction techniques – 1984 1991
I also investigated compatibility between equivalences induced by temporal logics and behavioral equivalences used in process calculi (the “Adequacy Problem” defined by R. Milner). This led to several journal papers.
Some of these results are used for the combination of model reduction techniques and model checking techniques in CADP and IF.
Abstraction Techniques – 19831994
In my paper on “Property Preserving Homomorphisms of Transition Systems”, presented at the workshop on "Logic of Programs", 1983, I was the first to study propertypreserving abstraction techniques by relating modelchecking and abstract interpretation founded by P&R Cousot. This work has been the starting point for collaborations with several researchers, including S. Graf, H. Saidi, and S. Bensalem. A comprehensive version of the theoretical results can be found here.
The results about using abstraction have been extended and successfully applied in the Inverst tool developed by S. Bensalem and Y. Lakhnech at Verimag.
This work has also influenced other tools such as SAL, developed at SRI.
Timed and Hybrid Systems  19911999
I developed, in collaboration with T. Henzinger, X. Nicollin and S. Yovine, the first symbolic modelchecking algorithm for the verification of TCTL. This algorithm has been implemented in the Kronos tool at Verimag.
The Kronos tool has been extensively and successfully used for the verification of critical realtime systems for the PATH project by S. Tripakis and S. Yovine, in the framework of collaboration with UC Berkeley (19972001).
Kronos is, with UPAAL, one of the two existing widely used model checking tools for timed systems.
I also worked on the verification of hybrid systems, in collaboration with researchers from Verimag and R. Alur and T Henzinger.
These general results are complemented by work on the verification of specific classes of hybrid systems, in particular in collaboration with Amir Pnueli.
Finally, in collaboration O. Maler and A. Pnueli, I produced results on the synthesis of controllers for timed systems.
These have been applied for schedulability analysis of realtime systems.
