Members
Research
Teaching

Formal Methods and Verification

The formal methods and verification group is one of the research groups of the Computer Science department at ULB's Science Faculty, and is lead by Thierry Massart and Jean-François Raskin. The team's research and teaching activities deal with rigorous methods that allow to design reliable computer systems. The latter are usually applied in the context of critical systems, such as embedded systems in transportation (e.g., trains, planes, cars), and plant's control systems.

The group has acquired an internationally acclaimed expertise, underpinned by numerous collaborations, and international research projects.

Members

Current researchers:
- Emmanuel FILIOT
- Gilles GEERAERTS
- Christian HERNALSTEEN
- Alexander HEUßNER
- Thierry MASSART
- Jean-François RASKIN
- Mathieu SASSOLAS
- Mahsa SHIRMOHAMMADI
Former members:
- Denis BOIGELOT
- Aldric DEGORRE
- Bram DE WACHTER
- Martin DE WULF
- Laurent DOYEN
- Pierre GANTY
- Alexandre GENON
- Raffaella GENTILINI
- Nayiong JIN
- Gabriel KALYON
- Steve KREMER
- Tristan LE GALL
- Nicolas MARKEY
- Nicolas MAQUET
- Cédric MEUTER
- Anthony PIRON
- Frédéric SERVAIS
- Nathalie SZNAJDER
- Laurent VAN BEGIN
- Eric VAN NUFFEL

Research

Principal Research Areas

hybrid and real-time systems;
infinite state systems, such as Petri nets or well-structured transition systems;
antichain-based model checking (see page on antichain-based techniques);
game theory (imperfect information, quantitative methods);
game theory based/quantitative approaches to model checking & synthesis;
testing and monitoring;
specification and validation of industrial critical systems.

Publications

Visit the website of the Centre Fédéré en Vérification for an up-to-date list of the group's publications. Alternatively, 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-Hainaut, 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 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

Further, the group is a partner in the following international and national projects:

ERC inVEST (Foundations for a Shift from Verification to Synthesis)
Quasimodo (Quantitative System Properties in Model-Driven-Design of Embedded Systems)
PAI-MoVES (Modeling, Verification and Evolution of Software)
GASICS (Games for Analysis and Synthesis of Interactive Computational Systems)

Teaching

Members of the group also actively teaching formal methods as part of the program Master in Computer Science, and Master in Computer Engineering at the ULB.

Traditionally, the group offers the following courses:

In this context, the group proposes topics for master's thesis (for the students at ULB only) and internships. We are also always happy to welcome highly motivated graduate and PhD students for short or long term internships. Do not hesitate to contact G. Geeraerts, T. Massart, or J.F. Raskin.