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-Saclay
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à).
