Formal Methods and Verification Research Group

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.

Publications

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

Tools

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.

Seminar

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

Collaborations

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.

Projects

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