SUZANNE Thibault

Docteur
Équipe : APR
Date de départ : 31/10/2017
Direction de recherche : Antoine MINÉ

Vérification par interprétation abstraite en mémoire faiblement cohérente

Parmi les méthodes de certification de logiciels critiques, l'analyse statique vise à établir l'absence d'erreurs dans toutes les exécutions possibles d'un programme donné. L'interprétation abstraite fournit un cadre théorique général permettant de concevoir de telles analyses sûres par construction : elles n'oublient aucun comportement de la cible.
Nous nous intéressons dans cette thèse à la vérification de programmes concurrents s'exécutant dans des modèles mémoire dits faiblement cohérents. En plus des exécutions séquentiellement cohérentes générées par les entrelacements des processus, ces modèles autorisent des comportements contre-intuitifs rendant le raisonnement d'autant plus difficile.
Nous proposons des domaines abstraits dédiés pour analyser les programmes s'exécutant dans de tels domaines. Résultats expérimentaux à l'appui, nous montrons comment ces domaines permettent, à l'aide de méthodes de calcul adaptées, de vérifier avec précision la correction d'algorithmes classiques de programmation concurrente.
Pour permettre un meilleur passage à l'échelle, nous étendons ces travaux à la conception d'une analyse modulaire. Nous montrons par l'expérience comment, en tirant profit d'abstractions spécifiques et d'une stratégie d'itération optimisée, cette méthode permet d'analyser efficacement des programmes comportant un plus grand nombre de processus.
Nous définissons finalement des domaines permettant d'inférer avec précision des relations spécifiques au modèle mémoire afin de pouvoir certifier des programmes aux invariants complexes.
Soutenance : 26/02/2019 - 14h - Salle W, École Normale Supérieure : 45 rue d'Ulm, 75005 Paris
Membres du jury :
M. David Pichardie (ENS Rennes, Irisa), [Rapporteur]
M. David Monniaux (Verimag, CNRS), [Rapporteur]
M. Antoine Miné (LIP6, Sorbonne Université)
M. Emmanuel Chailloux (LIP6, Sorbonne Université)
M. Luc Maranget (Inria Paris)
M. Xavier Rival (École normale supérieure, Inria)

Publications 2016-2019

 Mentions légales
Carte du site |