SALL Boubacar Demba

PhD student at Sorbonne University
Team : APR
https://lip6.fr/Boubacar.Sall

Supervision : Emmanuel CHAILLOUX
Co-supervision : PESCHANSKI Frédéric

Programmation impérative par raffinements avec l'assistant de preuve Coq

Cette thèse s’intéresse à la programmation certifiée correcte dans le cadre formel fourni par l’assistant de preuve Coq. La démarche de programmation étudiée consiste à procéder par raffinements successifs, et permet d’aboutir à un résultat qui est correct par construction. Le langage de programmation considéré est un langage impératif simple (avec affectations, alternatives, séquences, et boucles) auquel nous associons une sémantique relationnelle exprimée dans un cadre prédicatif et adapté à un plongement dans la théorie des types. Nous étudions la relation entre d’une part la sémantique prédicative et relationnelle que nous avons choisie, et d’autre part une approche plus classique dans le style de la logique de Hoare. En particulier, nous montrons que les deux approches ont en théorie la même puissance. La démarche que nous étudions consiste à certifier, avec l’aide d’un assistant de preuve, les raffinements successifs permettant de passer de la spécification au programme. Nous nous intéressons donc aussi aux techniques de preuve permettant en pratique d’établir la validité des raffinements. Plus précisément, nous utilisons un calcul de la plus faible pré-spécification jouant ici le rôle du calcul de la plus faible pré-condition dans les approches classiques. Afin que l’articulation des étapes de raffinement reste aussi proche que possible de l’activité de programmation, nous formalisons un langage de développement qui permet de décrire l’arborescence des étapes de raffinement, ainsi qu’une logique permettant de raisonner sur ces développements, et de garantir leur correction. Enfin, la théorie de la programmation par raffinements que nous avons développée a été entièrement mécanisée avec l'assistant de preuve Coq.


Phd defence : 10/01/2020

Jury members :

M. Tristan CROLARD - (CNAM) [Rapporteur]
M. Marc FRAPPIER - (Université de Sherbrooke) [Rapporteur]
Mme Maria Virginia APONTE - (CNAM)
M. Sylvain BOULMÉ - (Université Grenoble Alpes)
M. Emmanuel CHAILLOUX - (Sorbonne Université)
M. Emmanuel LEDINOT - (Thales Recherche & Technologie)
M. Antoine MINÉ - (Sorbonne Université)
M. Frédéric PESCHANSKI - (Sorbonne Université)

Departure date : 10/02/2020

2017-2020 Publications