Prochain Exposé
Thursday December 17, 11AM Paris/France. (Playback)
Lelio Brun (Inria, ENS, France)
Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset (Slides)
Specifications based on block diagrams and state machines are used to
design control software, especially in the certified development of
safety-critical applications.
Tools like SCADE and Simulink/Stateflow are equipped with compilers that
translate such specifications into executable code.
They provide programming languages for composing functions over streams
as typified by dataflow synchronous languages like Lustre.
In this work we present Vélus, a Lustre compiler verified in the
interactive theorem prover Coq.
We develop semantic models for the various languages in the compilation
chain, and build on the verified CompCert C compiler to generate
executable code and give an end-to-end correctness proof.
The main challenge is to show semantic preservation between the dataflow
paradigm and the imperative paradigm, and to reason about byte-level
representations of program states.
We treat, in particular, the modular reset construct, a primitive for
resetting subsystems.
This necessitates the design of suitable semantic models, compilation
algorithms and corresponding correctness proofs.
We introduce a novel intermediate language into the usual clock-directed
modular compilation scheme of Lustre.
This permits the implementation of compilation passes that generate
better sequential code, and facilitates reasoning about the correctness
of the successive transformations of the modular reset construct.
Exposés des semaines suivantes
Vos propositions sont les bienvenues !