I am a CNRS researcher at Irisa, Rennes, in the SUMO team.

At the time of writing, my official complete affiliation is the following:

Univ Rennes, Inria, CNRS, IRISA

Research Interests

  • Formal verification, model checking, controller synthesis, game theory, discrete-event systems
  • Automata theory, timed automata, Markov decision processes, (non-zero sum) games on graphs

PhD Students

  • Victor Roussanaly (defended in 2020) jointly supervised with N. Markey
  • Suman Sadhukhan (From Fall 2018) jointly supervised with N. Bertrand and N. Markey
  • Arthur Queffelec (From Fall 2018) jointly supervised with F. Schwarzentruber
  • Abdul Majith (From Jan 2019) jointly supervised with H. Marchand and Thai Dinh-Bui.




ANR Ticktac (2019-2023)


Tiamo: A timed automata model checker

Symrob: Symbolic robustness analysis tool for timed automata.

AbsSynthe: A tool for synthesizing circuits with safety specifications. See the synthesis competition, the source code and its developer Guillermo A. Perez.


Verification of Complex Systems

Lab sessions for: Analyse et Conception Formelles


  • Address Irisa
    Campus Universitaire de Beaulieu
    35042 Rennes cedex - France
  • Phone +33 (0)2 99 84 22 80
  • Fax +33 (0)2 99 84 71 71