LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » Links » LIP6 events

GdT programmation / séminaire IRILL / séminaire APRRSS

Verifying clock-directed modular code generation for Lustre


03/24/2016
Speaker(s) : Pierre-Evariste Dagand (WHISPER/LIP6, UPMC)
This work addresses the compilation pass that transforms synchronous dataflow programs into imperative programs. The challenge is to move from a dataflow semantics, where programs manipulate streams of values, to an imperative one, where programs perform stateful computations. We specify and verify in the Coq interactive theorem prover a code generator that handles the key aspects of Lustre including nodes and delays.
More details here
Emmanuel.Chailloux (at) nulllip6.fr
 Mentions légales
Site map |