Presentation
I am a post-doctorate in computer science. Since September 2012, I am working at INRIA Rennes/IRISA in the TAMIS project with Axel Legay. I have also been part of the ESTASYS, TRISKELL and DISTRIBCOM groups.
Previously, from January 2011 until August 2012, I worked for the danish research center MT-LAB. I worked at the IT University of Copenhagen with Andrzej Wąsowski and at Aalborg University with professor Kim G. Larsen. In 2010, I worked in the Software Technologies Laboratory of the University of Florence in Italy, with professor Enrico Vicario
From 2006 to 2009 I was a Ph.D student in Control Theory and Applied Computer Science of the University of Nantes, in the french laboratory IRCCyN. I was working in the Real Time Systems team with Olivier (H.) Roux, David Delfieu and Didier Lime.
I defended my Ph.D thesis the 27th of November 2009 at the IRCCyN in Nantes. The title is:
"Model-checking and unfoldings of parametric time Petri nets"
The manuscript and the slides of the defense are available (in french) on HAL or here.
I have been involved in the following events:
- SiSoS'16 conference : PC Member
- FORMATS'15 conference : PC Member
- FORMATS'14 conference : PC Member
- EXPRESS/SOS 2013 workshop : PC Member
- RV'13 conference : Local organizer
- QMC Ph.D school : Local organizer
Research
I am working on quantitative verification of critical systems using formal methods. Using model-based approaches, I try to verify formal specifications of the system's correctness. We apply rigorous mathematical analyses on these models, for instance to measure execution times or energy consumption, to estimate probabilities of failures, or optimize performances by synthesizing temporal or stochastic parameters. These works have practical applications in embedded systems, used in astronautics, transports (avionics, cars ...) or medical equipment. I study the following approaches:
- Specification of real-time systems using time Petri nets and timed automata (TIOA).
- Specification of adaptive systems.
- Model-checking, and controller synthesis with timed games.
- Statistical model-checking.
- Robustness and implementability.
- Parametric methods.
- True concurrency preservation methods such as unfoldings.
Tools
I have participated to the development of the following tools:
- PLASMA LAB, is a platform for statistical model-checking of stochastic models.
- PyECDAR, a tool written in python for the analysis of timed specifications and timed games. It implements some functionalities of the tool ECDAR. Additionally, it features special techniques for analysing robust specifications.
- QUAIL, a tool for the quantitative analysis of imperative languages.
- Romeo, a software studio for time Petri net analysis. It allows to edit and to simulate time Petri nets and can perform on-the-fly verification of temporal logic properties. I have developed the use of Parametric TPNs in Romeo as well as the computation of symbolic time unfoldings.
- PyPPL: Python bindings using the Parma Polyhedra Library with parametric timed automata.
- LLbox, a tool that can perform temporal analysis of the scenarii of a TPN using linear logic.