LIP6 CNRS Sorbonne Université
Direct Link LIP6 » News » PhD students

SALL Boubacar Demba

PhD graduated
Team : APR
Localisation : Campus Pierre et Marie Curie
    Sorbonne Université - LIP6
    Boîte courrier 169
    Couloir 25-26, Étage 3, Bureau 303
    4 place Jussieu
    75252 PARIS CEDEX 05
    FRANCE
Tel: +33 1 44 27 88 16, Boubacar.Sall (at) nulllip6.fr

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.

Defence : 10/01/2020 - 14h - Campus Jussieu, Salle Jacques Pitrat (25-26/105)

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é)

2017-2020 Publications

 Mentions légales
Site map |