< Retour au sommaire

Compilation formellement vérifiée d'un langage pour le calcul formel

Josué Moreau le

Lieu: salle 1073, bât 862

Suivre en visio

Abstract

Nous présentons une ébauche de langage de bas niveau ayant pour but de pouvoir écrire les algorithmes de base du calcul formel. Les structures de données manipulées par ces algorithmes étant principalement des tableaux, c’est sur ces derniers que notre langage se concentre. Nous présentons sa sémantique qui a été formalisée en Coq. Elle a été conçue dans l’optique d’être sûre, en éliminant certains comportements indéfinis tels que l’accès en dehors des bornes d’un tableau. Un autre objectif de cette sémantique est de simplifier la preuve de programme, par exemple en distinguant tableaux mutables et immuables. Nous nous intéressons enfin à la compilation formellement vérifiée de ce langage vers un langage assembleur. Pour atteindre cet objectif, nous avons écrit un compilateur de notre langage vers le langage intermédiaire C#minor de CompCert et nous avons prouvé formellement la préservation de la sémantique lors de cette traduction.