François LAROUSSINIE

Statut

Professeur des universités

Promotion

Membre honoraire 2008

Établissement

Université Paris Cité

Secteur disciplinaire

Sciences et Technologies de l'Information et de la Communication

Spécialité

Informatique

Thématique

► Vérification
► Model checking
► Logique temporelle
► Automat. temporisé
► Contrôle

Présentation

Je travaille au laboratoire LIAFA (UMR CNRS -- Paris 7) sur la vérification formelle de systèmes informatiques. Je m’intéresse notamment à la vérification automatique : on modélise le système à vérifier avec un modèle mathématique (un automate, un réseau de Petri,…), on exprime les propriétés de correction dans un langage formel (par exemple avec une logique temporelle) puis on vérifie (à l’aide d’un algorithme de model-checking) si le modèle satisfait ou non sa spécification. Je m’intéresse à ces différents aspects : la recherche de modèles expressifs pour décrire le comportement de ces systèmes et l’étude de leur expressivité et de leur complexité.

Membre junior de la promotion 2008.