I am mainly interested in formal verification, with a focus on timed systems on one hand, and on properties on infinite words on the other hand. The main axis for my research resides in the development of efficient techniques to verify and synthesize such systems. This leads me to implement the algorithms I design, and to evaluate their performance against other proposed methods.
Synthesis consists in (automatically) building a system that meets a given formal specification. It allows to design systems that are correct by construction, thus avoiding all possible flaws of hand-made design (tests, debugging, formal verification...). Synthesis also detects unrealizable specifications, and is useful in detecting over-constrained designs. The synthesis problem relates to game theory, as it can be seen as a game between the designer, who tries to enforce the specification, and a spoiling opponent. I am interested in synthesis of systems from LTL (and ω-regular) properties, based on parity games.
Timed systems model systems featuring real-time constraints. Due to the continuous nature of time, the first step towards their analysis is to somehow discretize them. Such discretization techniques mostly rely on polytopes that partition the clock-valuation space. But this step raises numerous question, regarding the soundness of discretization, with respect to a class of properties of interest, and regarding the complexity required to handle and analyze the discretezed system. I also consider extensions of timed systems, especially with weights to model the consumption of some resource, and also their game counterparts.