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

Previously, I was a Post-doc at ULB, and member of the ERC inVEST project.
See the verification group at ULB.

We have a fully funded PhD position on controller synthesis for adaptive systems using game theory. You can apply immediately.

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




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.

Recent Talks

All talks

Program Committees


See 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