---

Responsable: Ahmed Bouajjani    Page personnelle

---

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 permanents

Eugène Asarin	Professeur	PARIS 7
Ahmed Bouajjani	Professeur	PARIS 7
Aldric Degorre	Maître de conférence	PARIS 7
Constantin Enea	Maître de conférence	PARIS 7
Irene Guessarian	Professeur émérite	PARIS 6
Peter Habermehl	Maître de conférence	PARIS 7
Florian Horn	Chargé de recherche	CNRS
Yan Jurski	Maître de conférence	PARIS 7
François Laroussinie	Professeur	PARIS 7
Arnaud Sangnier	Maître de conférence	PARIS 7
Mihaela Sighireanu	Maître de conférence	PARIS 7
Tayssir Touili	Chargée de Recherche	CNRS

---

Postes temporaires

Michael Emmi	Post-doctorant	PARIS 7	[ 06 Oct 2010 - 06 Oct 2013 ]
Chunyan Mu	Post-doctorante	PARIS 7	[ 25 Oct 2012 - 01 Nov 2013 ]

---

Doctorants

Nicolas Basset	Doctorant	PARIS 7
Amit Dhar	Doctorant	PARIS 7
Antoine Durand-Gasselin	Doctorant	PARIS 7
Jad Hamza	Doctorant	PARIS 7
Fu Song	Doctorant	CNRS