My research work is related to distributed systems, software engineering and formal methods.

My goal is to provide verification tools dedicated to distributed systems and usable by engineers with little knowledge of the underlying techniques.

So, I try to make a bridge between standard specification notation such as UML or AADL and optimized verification techniques based on Model Checking and the Analysis of properties of the system. My work relies on Petri Nets but I am also focusing on other notations suitable to express behaviors of concurrent systems.

These past years, I have explored several techniques to increase the efficiency of model checking engines : intensive exploitation of symmetries in systems, various types of decision diagrams (and automated saturation), new classes of automata (Transition based Generalized Testing Automata), etc.

More recently I also focus my interested in the use of SAT solvers in the context of bounded model checking. We are investigating several techniques to speed up their execution : parallelization and exploitation of symmetries or other structural properties in the input CNF.

I also try to provide prototype implementations of these techniques in dedicated verification tools. It is thus possible to assess these with realistic problems. So far, I tackle applications such Middleware, Intelligent Transport Systems, Intrusion Detection Systems, or wireless sensor networks that are typical examples of complex distributed systems.