Full Professor - Professeur des Universités
HDR (Habilitation à Diriger Des Recherches)
Université Paris Saclay (formerly Paris Sud)
My research activities address formal methods in software development
cycle and in particular model-based testing, runtime verification, and parameterized model checking for concurrent and distributed systems.
I have a particular focus on behavioural models that are described by means of transition systems.
I have been particularly involved in the development of active testing methods that need to interact with the system under test and in the last years in monitoring approaches that only need to observe the system under test. I have proposed formal models to capture the specific features of composite sytems such as orchestration and choreographies for distributed systems. I work currently on attack tolerance framework to detect attack with passive methods and to bring countermeasures in order to enable the system to work despite the presence of the attack. Moreover, I am also involved in verification techniques for parameterized systems with model checking modulo theories. Recently, we have proposed a novel approach to deal with weak memory models.
My applicative domains are related to protocols such as Manets, cache coherence protocols and Web services.