Génération de code certifié pour Lustre

Abstract

Les compilateurs de langages schémas-blocs, comme Lustre ou Scade, utilisent souvent un langage intermédiaire entre le code flot de données source et le code impératif cible. Nous avons récemment implémenté et vérifié une fonction de traduction dans Coq d’un langage intermédiaire simple vers le langage Clight accepté par le compilateur CompCert. Le langage intermédiaire utilise une représentation idéalisée d’une mémoire hiérarchique, alors que Clight utilise un modèle de mémoire sophistiqué assez proche de la machine. Notre preuve de correction doit donc confronter les questions d’alignement, d’aliasing, et du padding. On se sert des prédicats de séparation développés dans CompCert pour résoudre ces problèmes.

Date
Nov 28, 2016 4:25 PM
Location
Laboratoire de Recherche en Informatique
Bât. 650 Ada Lovelace, rue Raimond Castaing
91190 Gif-sur-Yvette
Lélio Brun
Lélio Brun
Postdoctoral research scientist in Computer Science

My research interests include synchronous languages, functional programming and verified compilation.