Skip to Main content Skip to Navigation
Reports

Vers la certification du compilateur v5 d'Esterel dans Coq

Delphine Kaplan-Terrasse 1
1 TICK - Theory and Practice of Synchronous Reactive Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , MINES ParisTech - École nationale supérieure des mines de Paris
Résumé : Le compilateur v5 d'Esterel est basé sur un raffinement sémantique de la causalité correspondant aux «circuits constructifs» dans le domaine du matériel. La sémantique est présentée par un ensemble de règles d'inférence dans le style de la sémantique naturelle. Nous avons prouvé formellement la correction de la traduction d'une partie significative du langage en circuits au moyen du système de preuves Coq et de son interface utilisateur disponible dans Centaur. La nouvelle sémantique constructive d'Esterel a d'abord été écrite en Typol, donnant d'une part un interprète en Prolog et d'autre part une spécification en Coq. La traduction en circuit à la base du compilateur Esterel v5 a été directement spécifiée en Coq en utilisant l'ordre supérieur. Le principal travail a consisté à certifier le compilateur v5 en Coq en raisonnant sur ces spécifications.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00072540
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 10:13:53 AM
Last modification on : Thursday, September 24, 2020 - 4:00:25 PM
Long-term archiving on: : Sunday, April 4, 2010 - 11:12:39 PM

Identifiers

  • HAL Id : inria-00072540, version 1

Citation

Delphine Kaplan-Terrasse. Vers la certification du compilateur v5 d'Esterel dans Coq. RR-4092, INRIA. 2000. ⟨inria-00072540⟩

Share

Metrics

Record views

256

Files downloads

203