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 …
Lelio 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 …
PDF 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 …
PDF Project Slides Video DOI