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

Doctorat
Equipe : Toccata

Logique de séparation et vérification déductive

Début le 01/10/2008
Direction : FILLIÂTRE, Jean-Christophe

Ecole doctorale :
Etablissement d'inscription : Université Paris-Saclay

Lieu de déroulement : LRI-INRIA SACLAY

Soutenue le 12/12/2011 devant le jury composé de :
* Sandrine Blazy (rapporteur)
* Stéphane Demri
* Jean-Christophe Filliâtre
* Florent Hivert
* Christophe Ringeissen (rapporteur)

Activités de recherche :

Résumé :
Cette thèse s’inscrit dans la démarche de preuve de programmes à l’aide de vérification déductive. La vérification déductive consiste à produire, à partir des sources d’un programme, c’est-à-dire ce qu’il fait, et de sa spécification, c’est-à-dire ce qu’il est sensé faire, une conjecture qui si elle est vraie alors le programme et sa spécification concordent. On utilise principalement des démonstrateurs automatiques pour montrer la validité de ces formules. Quand on s’intéresse à la preuve de programmes qui utilisent des structures de données allouées en mémoire, il est élégant et efficace de spécifier son programme en utilisant la logique de séparation qui est apparu il y a une dizaine d’année. Cela implique de prouver des conjectures comportant les connectives de la logique de séparation, or les démonstrateurs automatiques ont surtout fait des progrès dans la logique du premier ordre qui ne les contient pas.

Ce travail de thèse propose des techniques pour que les idées de la logique de séparation puissent apparaître dans les spécifications tout en conservant la possibilité d’utiliser des démonstrateurs pour la logique du premier ordre. Cependant les conjectures que l’ont produit ne sont pas dans la même logique du premier ordre que celles des démonstrateurs. Pour permettre une plus grande automatisation, ce travail de thèse a également défini de nouvelles conversions entre la logique polymorphe du premier ordre et la logique multi-sortée du premier ordre utilisé par la plupart des démonstrateurs.

La première partie a donné lieu à une implémentation dans l’outil Jessie, la seconde a donné lieu à un participation conséquente l’écriture de l’outil Why3 et particulièrement dans l’architecture et écriture des transformations qui implémente ces simplifications et conversions.