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

Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels

Début le 14/09/2013
Direction : MARCHÉ, Claude

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

Lieu de déroulement : LRI - VALS

Soutenue le 30/03/2018 devant le jury composé de :
Directeur de thèse :
- Claude Marché, Directeur de recherche Inria, Saclay

Co-encadrant :
- Andrei Paskevich, Maître de conférences à l'Université Paris-Sud, Saclay

Rapporteurs :
- Sandrine Blazy, Professeure à l'Université de Rennes 1, Rennes
- Alexandre Miquel, Professeur à l'Universidad de la República, Montevideo

Examinateurs :
- Hubert Comon, Professeur à l'ENS Paris-Saclay, Saclay
- François Pottier, Directeur de recherche Inria, Paris

Activités de recherche :
   - Vérification déductive de programmes

Résumé :
Dans cette thèse, je propose de nouvelles méthodologies pour la vérification déductive de programme. Le résultat central de cette thèse est une méthode de preuve dite "par débogage", dont l'idée principale est de ne pas s'appuyer sur la structure syntaxique des programmes à vérifier mais plutôt celle de programmes auxiliaires écrits spécifiquement pour effectuer cette vérification. Cette méthode est en particulier applicable à la preuve de programme bas niveau de type assembleur, ainsi qu'à la preuve de compilateurs. La correction de cette approche est justifiée par un fondement théorique sur des jeux transfinis, ce qui permet en particulier de vérifier le bon comportement d'un programme lors d'une exécution infinie (et au-delà).