Équipe thématique


Responsable


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.


Annuaire

Nom@TéléphoneBureauFonctionPôleÉquipe
Asarin Eugène @ 01 57 27 92 34 4040 Professeur.e ASV verif
Beillahi Sidi-Mohamed @ 4060 Doctorant.e ASV verif
Bernardi Giovanni @ 01 57 27 93 38 4026 Maître.sse de conférence PPS , ASV preuves , systemes , verif
Biswas Ranadeep @ 4060 Doctorant.e ASV verif
Bouajjani Ahmed @ 01 57 27 92 64 4023 Professeur.e ASV verif
Bouillaguet Quentin @ 4021 Doctorant.e ASV verif
Cauderlier Raphael @ 4058 Post-Doctorant.e ASV verif
Degorre Aldric @ 01 57 27 92 32 4018 Maître.sse de conférence ASV verif
Delbianco German-Andres @ 01 57 27 94 07 4032 Post-Doctorant.e ASV verif
Enea Constantin @ 01 57 27 92 41 4028a Maître.sse de conférence ASV verif
Fang Bin @ 07 68 79 02 80 4061 Doctorant.e ASV verif
Guessarian Irène @ 01 57 27 92 59 4049 Professeur.e émérite ASV automates , verif
Habermehl Peter @ 01 57 27 92 58 3022 Maître.sse de conférence ASV automates , verif
Horn Florian @ 01 57 27 94 46 4039 Chargé.e de recherche - CNRS ASV automates , verif
Jeannerod Nicolas @ 01 57 27 92 22 3035 Doctorant.e avec mission d'enseignement PPS , ASV systemes , verif
Ji Kailiang @ 01 57 27 92 60 4057 Post-Doctorant.e ASV verif
Laroussinie François @ 01 57 27 92 42 4004 Professeur.e ASV verif
Long Teng @ 01 57 27 92 60 4054 Visiteur.euse ASV verif
Petri Gustavo @ 01 57 27 94 01 4021 Maître.sse de conférence - (en disponibilité) ASV verif
Pommellet Adrien @ 01 57 27 92 27 4052 ATER ASV verif
Sangnier Arnaud @ 01 57 27 92 58 3022 Maître.sse de conférence ASV verif
Sighireanu Mihaela @ 01 57 27 94 01 4021 Maître.sse de conférence ASV verif
Treinen Ralf @ 01 57 27 92 44 3021 Professeur.e PPS , ASV systemes , verif
Wang Chao @ 01 57 27 94 07 4032 Post-Doctorant.e ASV verif