Verified Compilation

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
Faites-vous confiance à votre thermostat ?
Certains systèmes logiciels qui interagissent avec le monde réel ne doivent échouer sous aucun prétexte, au risque de provoquer des …
Lélio Brun
Project Source Document
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