Lélio Brun's homepage
Lélio Brun's homepage
About
Publications
Talks
Projects
Experience
Teaching
Academic service
Contact
CV
Light
Dark
Automatic
Interactive Theorem Proving
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
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
×