Détails sur le séminaire

BBB room access code 349356

1er avril 2021 - 14h00
[FormalProofs] A formally-verified compiler from Esterel to circuits
par Lionel Rieg de VERIMAG / IIM Grenoble INP

Abstract: Esterel is a synchronous programming language (like Lustre or Signal) which can be compiled down to digital circuits, as described for instance in G. Berry's draft book: "The Constructive Semantics of Pure Esterel". The goal of this work is to provide a mechanized proof of the correctness of this compilation scheme.
In this talk, after a brief description of the Esterel high-level semantics, I will describe the chain of semantics linking this high-level semantics to the circuit one. Then, I will focus on the last two: the microstep semantics (based on Scott semantics) on the Esterel source code and its translation into the circuit semantics, with the related Coq challenges.

Contact | Plan du site | Site réalisé avec SPIP 3.2.16 + AHUNTSIC [CC License]

info visites 1876605