Page d'accueil du CNRS Page d'accueil de l'Université Paris Diderot Page d'accueil du LIAFA
LIAFA
Laboratoire d'Informatique Algorithmique: Fondements et Applications
CNRS et Université Paris Diderot
UMR 7089
   Annuaire      Contact      Accès au LIAFA      UFR d'informatique      Webmail   


English version




Page d'accueil de la Fédération de Recherche en Mathématiques de Paris Centre

Page d'accueil de la Fondation Sciences Mathématiques de Paris

Page d'accueil de Sciences En Marche
Modélisation et vérification
Séminaires



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
François Laroussinie Professeur PARIS 7
Gustavo Petri Maître de conférence PARIS 7
Arnaud Sangnier Maître de conférence PARIS 7
Mihaela Sighireanu Maître de conférence PARIS 7


Doctorants

Khanh-Huu-The Dam Doctorant PARIS 7
Marcio Diaz Doctorant PARIS 7
Bin Fang Doctorant PARIS 7
Huu-Vu Nguyen Doctorant PARIS 7
Adrien Pommellet Doctorant PARIS 7

 
 ©  LIAFA 1995, dernière mise à jour: Janvier 2016 webmestre[at]liafa.univ-paris-diderot.fr