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 of Parosh Abdulla, Uppsala University, Sweden;
- the group of Véronique Bruyère, University of Mons, Belgium;
- the group of Franck Cassez at the IRCyN, Ecole Centrale de Nantes, France;
- the group of Krishendu Chatterjee, IST Austria;
- the group of Giorgio Delzanno, DISI, University of Genova, Italy;
- the group of Thomas A. Henzinger, IST Austria;
- the VerTeCs group of Thierry Jéron, IRISA-INRIA, France;
- the group of Kim G. Larsen, Aalborg University, Denmark;
- the Modeling and Verification group, LaBRI, Bordeaux, France;
- the group of Michael Leuschel, University of Düsseldorf, Germany;
- the department of CS and Engineering, IIT Bombay, India;
- the MoVe group, Laboratoire d’Informatique Fondamentale de Marseille (LIF), France;
- the Laboratoire Spécification et Vérification (LSV), ENS de Cachan, France;
- the Computing Laboratory, University of Oxford, UK;
- the group of Pierre-Yves Schobbens, University of Namur, Belgium;
- the Stanford Research Institute, California, USA;
- the Verimag, Grenoble, France.
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)
- GASSICS (ESF)
- 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