Résumé
Le séminaire a porté sur la formalisation et la preuve en Coq d’un générateur de code impératif pour un noyau du langage Lustre. Une telle vérification formelle pourrait avantageusement compléter les méthodes officielles de certification actuellement employées pour SCADE 6, qui intègre Lustre et une version restreinte d’Esterel. Même si le cœur du compilateur n’est qu’un petit morceau du système total, il est essentiel car tout bug engendré par ce cœur peut avoir des conséquences imprévisibles et potentiellement graves.
L’exposé a présenté la spécification et la vérification d’un générateur de code simple qui gère les traits principaux de Lustre : l’échantillonnage, les nœuds et les délais. La chaîne de génération de code intègre le compilateur C formellement vérifié CompCert pour produire le code assembleur final. Les garanties offertes par CompCert permettent d’étendre le théorème de correction de la traduction de Lustre à toute la chaîne de compilation des programmes Lustre vers l’assembleur.
