Recherche
Ces dernières années ont vu le développement d'un grand nombre d'outils de certification de logiciels utilisant la preuve de programme dont le but est de garantir la sûreté du programme (typage et terminaison) et de s'assurer de ses propriétés algorithmiques.
Le but de ma thèse est de concevoir des outils logiques en vue de développer un assistant de preuve de programmes ML intégrant des aspects impératifs (références, partage). Cet assistant devra permettre une gestion native des programmes de manière à raisonner sans avoir à les transformer au préalable. Mon point de départ a été PAF! un assistant à la preuve développé par S.Baro et P.Manoury dédié au fragment fonctionnel de ML. PAF! est basé sur une logique du 2e ordre à la AF2 et permet de prouver la terminaison d'un programme, en revanche il ne traite pas les effets de bord. Ce système est adapté à notre objectif car il permet un traitement distinct des programmes et des preuves, offrant ainsi la possibilité de certifier du code déjà écrit sans le modifier.
Il y a essentiellement deux manières d'intégrer les effets de bord à la preuve de programme : les transformations monadiques (WHY, Caduceus) et la logique de Hoare ou la logique modale dynamique qui en est une généralisation. C'est cette derrière approche, originale pour le traitement des langages à la ML, que j'ai adoptée.
Je me suis également intéressée aux travaux de recherche dédiés à la certification de programmes JavaCard et menés par l'équipe suédoise du KeY Project. J'ai pu constater des similarités inattendues avec l'approche de PAF! notamment concernant le rôle prépondérant de l'évaluation symbolique et l'utilisation de la logique dynamique. Ainsi mon projet de recherche a naturellement inclus l'adaptation des outils et des méthodes de KeY à la preuve de programme en ML, problème ouvert dans leur projet. Cela signifie d'une part adapter leurs outils au langage de programmation à la ML qui m'intéresse, un langage d'ordre supérieur avec référence. D'autre part, il a fallut également mettre au point un système de logique modale dynamique du 2nd ordre, MLDL, ce qui reste une approche originale pour la preuve de programmes ML. La cohérence de MLDL a été prouvée de manière sémantique au moyen d'un modèle de réalisabilité.
Actuellement, je travaille sur une extension de MLDL dédiée au typage des programmes.