I am a researcer at CNRS within Université de Rennes, in the SUMO team.

Research Interests

Formal verification, model checking, planning and controller synthesis, game theory, real-time systems
Timed automata, Markov decision processes, non-zero sum games

My current projects include the following
  • Automatic assume-guarantee reasoning for model checking (see CircAG)
  • Black-box testing for reactive systems using reinforcement learning (see RL-Tester)
  • Symbolic verification techniques for timed automata (see CAV19,TACAS23)
  • Formal verification of distributed algorithms (see TACAS17)

PhD Students

  • Victorien Desbois (From Fall 2023)
  • Thibaut Le Marre (From Fall 2023)
  • Nicolas Waldburger (From Oct 2021) jointly supervised with N. Bertrand and N. Markey
  • Abdul Majith (defended in 2022) jointly supervised with H. Marchand and Thai Dinh-Bui (Nokia - Bell Labs).
  • Suman Sadhukhan (defended in 2021) jointly supervised with N. Bertrand and N. Markey
  • Arthur Queffelec (defended in 2021) jointly supervised with F. Schwarzentruber
  • Victor Roussanaly (defended in 2020) jointly supervised with N. Markey


CV (possibly outdated)


ANR Ticktac (2019-2023)


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

Some of the tools I am developing are available on my Github profile.


Türkçe Akademik Teknik Terimler Sözlüğü


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