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.