Doctorat
Equipe : Vérification d'Algorithmes, Langages et Systèmes
Un système de types pragmatique pour la vérification déductive des programmes
Début le 01/10/2013
Direction : FILLIÂTRE, Jean-Christophe
Ecole doctorale : ED STIC 580
Etablissement d'inscription : Université Paris-Saclay
Lieu de déroulement : LRI VALS
Soutenue le 13/12/2016 devant le jury composé de :
Directeurs de thèse :
- M. Jean-Christophe Filliâtre, CNRS, Université Paris Sud
- M. Andrei Paskevich, Université Paris Saclay
Rapporteurs :
- Mme Sandrine Blazy, Université de Rennes 1
- M. Jorge Sousa Pinto, Universidade de Minho
Examinateurs :
- M. Giuseppe Castagna, CNRS, Université de Paris 7
- M. Jean Goubault-Larrecq, LSV, CNRS, ENS Cachan
- M. François Pottier, INRIA Paris
Activités de recherche :
- Vérification déductive de programmes
Résumé :
Ma thèse se place dans le contexte de la vérification déductive des
programmes et a pour objectif de formaliser un certain nombre
de concepts qui sont mis en œuvre dans l'outil de vérification Why3.
L'idée générale est d'explorer des solutions qu'une approche
à base de systèmes de types peut apporter à la vérification.
Nous commençons par nous intéresser à la notion du code fantôme, une
technique implantée dans de nombreux outils de vérification modernes, qui
consiste à donner à des éléments de la spécification les
apparences d'un code opérationnel. L'utilisation correcte du code fantôme
requiert maintes précautions puisqu'il ne doit jamais interférer avec le
reste du code. La première contribution de ma thèse consiste à proposer un
cadre formel pour le code fantôme, en illustrant comment un système de types
avec effets en permet une utilisation à la fois correcte et expressive.
Puis nous nous intéressons à la vérification des programmes manipulant des
pointeurs. En présence d'aliasing, c'est-à-dire lorsque plusieurs pointeurs
manipulés dans un programme dénotent une même case mémoire, la spécification et
la vérification deviennent non triviales. Plutôt que de nous diriger vers des
approches existantes qui abordent le problème d'aliasing dans toute sa
complexité, mais sortent du cadre de la logique de Hoare, nous présentons un
système de types avec effets et régions singletons qui permet d'effectuer un
contrôle statique des alias avant même de générer les obligations de preuve.
Bien que ce système de types nous limite à des pointeurs dont l'identité
peut être connue statiquement, notre observation est qu'il convient à une
grande majorité des programmes que l'on souhaite vérifier.
Enfin, la troisième contribution de ma thèse est en rapport avec les questions
liées à la vérification de programmes conçus de façon modulaire. Concrètement,
nous nous intéressons à une situation où il existe une barrière d'abstraction
entre le code de l'utilisateur et celui des bibliothèques dont il dépend. Cela
signifie que les bibliothèques fournissent à l'utilisateur une énumération de
fonctions et de structures de données manipulées, sans révéler les détails de
leur implémentation. Le code de l'utilisateur ne peut alors exploiter ces
données qu'à travers un ensemble de fonctions fournies. Dans une telle
situation, la vérification peut elle-même être modulaire. Du côté de
l'utilisateur, la vérification ne doit alors s'appuyer que sur des invariants
de type et des contrats de fonctions exposés par les bibliothèques. Du côté de
ces dernières, la vérification doit garantir que la représentation concrète
raffine correctement les entités exposées, c'est-à-dire en préservant les
invariants de types et les contrats de fonctions. Dans ma thèse, j'ai exploré
en quoi un système de types permettant le contrôle statique des alias est un
ingrédient à la fois nécessaire et original de la vérification modulaire et le
raffinement des structures de données en Why3.
