Lélio Brun's homepage
Lélio Brun's homepage
About
Publications
Talks
Projects
Experience
Teaching
Academic service
Contact
CV
Light
Dark
Automatic
Publications
Type
Uncategorized
Conference paper
Date
2023
2022
2020
2018
2017
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, …
Lélio Brun
,
Christophe Garion
,
Pierre-Loïc Garoche
,
Xavier Thirioux
PDF
Cite
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
Cite
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
Cite
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
Cite
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 …
Timothy Bourke
,
Lélio Brun
,
Pierre-Évariste Dagand
,
Xavier Leroy
,
Marc Pouzet
,
Lionel Rieg
PDF
Cite
Project
Slides
Video
DOI
Cite
×