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) games on graphs

Current PhD Students

  • Victor Roussanaly (From Fall 2017) 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


Some slides (not up-to-date)



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. We have been winning the first prize in at least one category from 2014 to 2017 in the synthesis competition. See the source code and its main 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