Modélisation et vérification

Responsable : Ahmed Bouajjani

Thèmes de recherche

Les activités de l'équipe Modélisation et Vérification portent sur le développement d'approches algorithmiques pour la vérification de systèmes, des fondements théoriques aux outils de vérification innovants.

Les applications visées sont dans un spectre large comprenant les algorithmes distribués, les réseaux dynamiques de processus communicants, les systèmes temps-réel, les systèmes embarqués critiques, les programmes avec structures de données complexes, les programmes concurrents, etc.

Les approches adoptées sont généralement basées sur l'utilisation (1) de modèles formels pour la description à un certain niveau d'abstraction des comportements des systèmes étudiés, (2) de spécifications formelles pour la description des propriétés que doivent satisfaire ces systèmes, et (3) de méthodes algorithmiques soit pour établir la correction, soit pour détecter des comportements illicites, d'un système par rapport à sa spécification.

Les modèles et les formalismes de spécification sont de manière générale de type automate (finis, à piles/files, à horloges/compteurs, etc.) ou logique (temporelle, monadique de premier/second ordre, point fixe, etc.), et les problèmes de la vérification sont souvent ramenés à des problèmes de décision sur ces formalismes (accessibilité/langage vide pour les automates, satisfaisabilité pour les logiques, stratégies gagnantes pour les jeux, etc). Se pose alors la question de la décidabilité et de la complexité de ces problèmes, et celle de développer des techniques basées sur le calcul de (sur/sous) approximations raffinables pour résoudre ces problèmes de manière efficace.

L'équipe a des compétences dans les domaines de la vérification de systèmes infinis, systèmes temporisés et hybrides, logiques temporelles, jeux et model-checking, model-checking quantitatif, vérification de programmes.

Membres

NomTéléphoneBureauFonctionMail
Asarin Eugène 01 57 27 92 34 4040 Professeur.e Mail
Bouajjani Ahmed 01 57 27 92 64 4023 Professeur.e Mail
Bouillaguet Quentin Doctorant.e Mail
Cauderlier Raphael 4058 Post-Doctorant.e Mail
Degorre Aldric 01 57 27 92 32 4018 Maître.sse de conférence Mail
Enea Constantin 01 57 27 92 41 4008b Maître.sse de conférence Mail
Fang Bin 4061 Doctorant.e Mail
Guessarian Irène 01 57 27 92 59 4049 Professeur.e émérite Mail
Habermehl Peter 01 57 27 92 29 4017 Maître.sse de conférence Mail
Horn Florian 01 57 27 94 46 4039 Chargé.e de recherche Mail
Laroussinie François 01 57 27 92 42 4004 Professeur.e Mail
Petri Gustavo 01 57 27 94 01 4021 Maître.sse de conférence Mail
Sangnier Arnaud 01 57 27 92 41 4008 Maître.sse de conférence Mail
Sighireanu Mihaela 01 57 27 94 01 4021 Maître.sse de conférence Mail
Wang Chao Post-Doctorant.e Mail