Méthodes Formelles et Vérification
Le service Méthodes Formelles et Vérification fait partie du Département d'Informatique de la Faculté des Sciences de l'Université Libre de Bruxelles. Le group est géré par Thierry Massart and Jean-François Raskin. Notre équipe consacre ses efforts de recherche et d'enseignement aux méthodes rigoureuses et automatiques qui permettent de concevoir des systèmes informatiques fiables. Ces méthodes trouvent des applications naturelles dans la conception de systèmes informatiques critiques, comme les systèmes de contrôle embarqués dans les moyens de transport (métros, avions, voiture), les systèmes de contrôle de production (dans un cadre industriel), etc.
Notre groupe jouit d'une expertise internationallement reconnue, comme en témoigne nos nombreuses collaborations, ainsi que les projets de recherche internationaux auxquels nous participons.
Membres
- Membres actuels:
- Anciens membres:
- Denis BOIGELOT
- Aldric DEGORRE
- Bram DE WACHTER
- Martin DE WULF
- Laurent DOYEN
- Pierre GANTY
- Alexandre GENON
- Raffaella GENTILINI
- Nayiong JIN
- Gabriel KALYON
- Stever 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
Récherche
Thèmes de Récherche
- systèmes hybrides et temps-réels;
- systèmes à espaces d'états infinis, comme les réseaux Petri ou les systèmes bien structurés;
- model checking basé sur des antichaînes (voyez la page en anglais sur les techniques basés sur des antichaînes);
- théorie des jeux (avec information imparfait, méthodes quantitatives);
- model checking & synthèse basé sur des jeux;
- test et monitoring;
- spécification et validation des systèmes industriels.
Publications
Regardez la page web du Centre Fédéré en Vérification pour une liste actuelle des publications du groupe. Autrement, n'hésitez pas à visiter les pages personelles des membres du groupe.
Outils
Notre groupe développe et maintient plusieurs outils de vérification assistée par ordinateur. Ils sont référencés sur une page dédiée (en anglais).
Séminare
Visitez la page du séminaire pour des détails sur le planning.
Collaborations
Le groupe entretient des collaborations régulières avec les Universités et centres de recherche en Belgique et ailleurs. Il est membre fondateur du Centre Fédéré en Vérification.
Actuellement, nous collaborons regulièrement avec :
- le groupe du Parosh Abdulla, Université Uppsala, Suède;
- le groupe du Véronique Bruyère, Université de Mons-Hainaut, Belgique;
- le groupe du Franck Cassez à l'IRCyN, Ecole Centrale de Nantes, France;
- le groupe du Krishendu Chatterjee, IST Austria, Autriche;
- le groupe du Giorgio Delzanno, DISI, Université Genova, Italie;
- le groupe du Thomas A. Henzinger, IST Austria, Autriche;
- VerTeCs, le groupe du Thierry Jéron, IRISA-INRIA, France;
- le groupe du Kim G. Larsen, Université Aalborg, Danemark;
- le group Modélisation et Vérification, LaBRI, Bordeaux, France;
- le groupe du Michael Leuschel, Université de Düsseldorf, Allemagne;
- le Laboratoire Spécification et Vérification (LSV), ENS de Cachan, France;
- le Computing Laboratory, Université de Oxford, Royaume-Uni;
- le groupe du Pierre-Yves Schobbens, FUNDP Namur, Belgique;
- le Stanford Research Institute, Californie, États-Unis;
- le Verimag, Grenoble, France.
Projets
En plus, notre groupe participe activement aux projets de recherche suivants:
- 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)
Enseignement
Les membres de notre groupe enseignent les méthodes formelles et la vérification dans différents cours qui sont dispensés aux étudiants du MA en sciences informatique, et du MA en ingénieur civil informaticien.
Traditionnellement, le groupe offre les cours suivants:
- INFO-F-410: Concéption des Systèmes Embarqués
- INFO-F-412: Vérification 1
- INFO-F-513: Vérification 2
Notre groupe propose également des sujets de stage et de mémoire, en accord avec les thèmes de recherche du service. En fonction du suejt, les stages peuvent se dérouler dans un laboratoire à l'étranger ou en Belgique, avec lequel nous collaborons. N'hésitez pas à contacter G. Geeraerts, T. Massart ou J.F. Raskin.
