Séminaire Cambium, Inria Paris
                                     BJ09
                         Vendredi 14 novembre, 10h30

                                Paul Jeanmaire

               Stream semantics of synchronous block-diagrams,
                 application to a formally verified compiler

Lustre and Scade are synchronous dataflow languages. Their static clock types
allow them to be compiled to code that executes in bounded time and memory,
which is a significant advantage for safety-critical systems. Vélus is a
verified compiler for Lustre/Scade. It provides a proof, based on the definition
of formal semantics for each intermediate language, that a Lustre program and
its translation into Clight (the language supported by CompCert) have identical
input/output behaviors.
In this presentation, I will describe a new model of the input language's
dataflow kernel, based on a synchronous denotational semantics. I will detail
the main challenges we faced while encoding this functional model in the Rocq
proof assistant, where explicit computation of fixpoints of mutually recursive
stream equations requires particular care. I will show how this model relates to
the existing relational model in Vélus, reinforcing the main correctness theorem
of the compilation.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct
                            via le lien ci-dessus.