Français Anglais
Accueil Annuaire Plan du site
Accueil > Production scientifique > Thèses et habilitations
Production scientifique
Doctorat de

Doctorat
Equipe : Vérification d'Algorithmes, Langages et Systèmes

Outils et techniques pour la vérification de programmes impératives modulaires

Début le 01/05/2015
Direction : FILLIÂTRE, Jean-Christophe

Ecole doctorale : ED STIC 580
Etablissement d'inscription : Université Paris-Sud

Lieu de déroulement : LRI - VALS

Soutenue le 10/12/2018 devant le jury composé de :
Directeur de thèse:
- M. Jean-Christophe FILLIATRE, CNRS

Rapporteurs :
- M. Jorge SOUSA PINTO, Universidade do Minho
- M. Wolfgang AHRENDT, Chalmers University of Technology

Examinateurs :
- Mme Catherine DUBOIS, Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise
- Mme Mihaela SIGHIREANU, Université Paris Diderot
- M. Xavier LEROY, INRIA
- M. Laurent FRIBOURG, CNRS

Activités de recherche :

Résumé :
Cette thèse se place dans le cadre des méthodes formelles et plus précisément dans celui de la vérification déductive et du système Why3. Ce dernier fournit un ensemble d'outils pour la spécification, l'implémentation et la vérification à l'aide de démonstrateurs externes. Why3 propose en particulier un langage de programmation adapté à la preuve, appelé WhyML. Un aspect important de ce langage est le code fantôme, à savoir des éléments de programme introduits exclusivement pour les besoins de la spécification et de la preuve. Pour obtenir un code exécutable, le code fantôme est éliminé par un processus automatique appelé extraction. L'une des contributions principales de cette thèse est la formalisation et l'implémentation du mécanisme d'extraction de Why3. La formalisation consiste à montrer que le programme extrait préserve la sémantique du programme de départ, en s'appuyant notamment sur un système de types avec effets. Ce mécanisme d'extraction a été utilisé avec succès pour obtenir plusieurs modules OCaml corrects par construction, dans le cadre d'une bibliothèque vérifiée de structures de données et d'algorithmes. Cet effort de preuve a conduit à deux autres contributions de cette thèse. La première est une technique systématique pour la vérification de structures avec pointeurs, à l'aide de modèles du tas délimités. Une preuve entièrement automatique d'une structure union-find a pu être obtenue grâce à cette technique. La seconde contribution est un moyen de spécifier un algorithme d'itération indépendamment de son implémentation. Plusieurs curseurs et itérateurs d'ordre supérieur ont été spécifiés et vérifiés en utilisant cette approche.