Direction de recherche : Emmanuel CHAILLOUX

Co-encadrement : 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.

Publications 2017-2020

• 2020
  • B. Sall : “Programmation impérative par raffinements avec l’assistant de preuve Coq”, soutenance de thèse, soutenance 01/10/2020, direction de recherche Chailloux, Emmanuel, co-encadrement : Peschanski, Frédéric (2020)
• 2019
  • B. Sall, F. Peschanski, E. Chailloux : “A Mechanized Theory of Program Refinement”, ICFEM 2019 - 21^st International Conference on Formal Engineering Methods, vol. 11852, Lecture Notes in Computer Science, Shenzhen, China, pp. 305-321, (Springer) (2019)
• 2017
  • B. Sall, F. Peschanski, E. Chailloux : “Analyse de Bytecode par Raffinement”, Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'2017), Montpellier, France (2017)