Principal Research Areas

  • mathematical foundations of reactive synthesis
  • automata-based synthesis
  • hybrid and real-time systems;
  • infinite state systems, such as Petri nets or well-structured transition systems;
  • antichain symbolic methods;
  • game theory (imperfect information, quantitative methods);
  • infinite-state games
  • automata with outputs (transducers, quantitative automata, register automata,…)
  • testing and monitoring;
  • specification and validation of industrial critical systems.


We refer to the individual pages of the members of the group.


The group has developed a variety of computer-aided verification tools, e.g., for antichain-based approaches or well-structured transition systems. See the dedicated tool page for more details.


Please refer to the seminar’s page for a detailed schedule.


The group maintains a wide range of collaborations with other research groups in Belgium and abroad. It is also founding member of the Centre Fédéré en Vérification, a virtual center that regroups all the teams interested in computer-aided verification of (French-speaking) Belgium.

Currently, we are collaborating regularly with:


The group is or has been involved in the following international and national projects:

  • ERC inVEST: Foundations for a Shift from Verification to Synthesis
  • Cassting: Collaborative Adaptive Systems SynThesIs using Non-zero sum Games (EU FP7)
  • FORESt: Formal verificatiOn techniques for REal-time Scheduling problems (PDR FNRS)
  • Quasimodo Quantitative System Properties in Model-Driven-Design of Embedded Systems
  • SyVerLo: Synthesis and Verification of Real-time Logics (PDR FNRS)
  • Non-Zero Sum Graph Games: Applications to Reactive Synthesis and Beyond (Action de Recherche Concertée de la CFWB)
  • Subgame Perfection in Graph Games (PDR-FNRS)
  • Verifying Learning Artificial Intelligence Systems (Excellence of Science program FNRS-FWO)
  • On the verification of rationality and under rationality assumptions, with applications to reactive systems (PDR-FNRS)
  • MoVeS: Interuniversity attraction pole