1

Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation
Model-based design tools like SCADE Suite and Simulink are often used to design safety-critical embedded software. Consequently, …
PDF Project Slides DOI
Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset
Specifications based on block diagrams and state machines are used to design control software, especially in the certified development …
Timothy Bourke, Lélio Brun, Marc Pouzet
PDF Project Slides Video DOI
Towards a Verified Lustre Compiler with Modular Reset
This paper presents ongoing work to add a modular reset construct to a verified Lustre compiler. We present a novel formal …
Timothy Bourke, Lélio Brun, Marc Pouzet
PDF Project Slides DOI
A Formally Verified Compiler for Lustre
The correct compilation of block diagram languages like Lustre, Scade, and a discrete subset of Simulink is important since they are …
PDF Project Slides Video DOI