version française

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

• Faculty:
  • Emmanuel FILIOT
  • Gilles GEERAERTS
  • Thierry MASSART
  • Jean-François RASKIN
• Associated staff:
  • Raphaël BERTHON
  • Debraj CHAKRABORTY
  • Léo EXIBARD
  • Shibashis GUHA
  • Nicolas MAZZOCCHI
  • Marie VAN DEN BOGAARD
  • Sarah WINTER
• Former members: Arthur MILCHIOR, Ismaël JECKER, Luc DARTOIS, Mickael RANDOUR, Guillermo A. PÉREZ, Denis BOIGELOT, Romain BRENGUIER, Lorenzo CLEMENTE, Aldric DEGORRE, Amit Kumar DHAR, Bram DE WACHTER, Martin DE WULF, Laurent DOYEN, Pierre GANTY, Alexandre GENON, Raffaella GENTILINI, Axel HADDAD, Christian HERNALSTEEN, Alexander HEUßNER, Hsi-Ming Ho, Paul HUNTER, Nayiong JIN, Gabriel KALYON, Stever KREMER, Engel LEFAUCHEUX, Tristan LE GALL, Stéphane LE ROUX, Pritha MAHATA, Nicolas MAQUET, Nicolas MARKEY, Cédric MEUTER, Benjamin MONMEGE, Arno PAULY, Thi-Van-Anh NGUYEN, Anthony PIRON, Ocan SANKUR, Mathieu SASSOLAS, Frédéric SERVAIS, Mahsa SHIRMOHAMMADI, Amélie STAINER, 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;
• 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, 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

Further, the group is a partner 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)
• FORESt (Formal verificatiOn techniques for REal-time Scheduling problems

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:

• INFO-F-410: Embedded Systems Design
• INFO-F-412: Verification 1
• INFO-F-513: Verification 2

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.

Contact

NO building, 8th floor
Campus de la Plaine
ULB CP212, boulevard du Triomphe, 1050 Bruxelles

---

Last update: R. Berthon 22 MARCH 2019