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 used to program critical embedded control software. We describe the specification and verification in an Interactive Theorem Prover of a compilation chain that treats the key aspects of Lustre: namely, sampling, nodes, and delays. Building on CompCert, we show that repeated execution of the generated assembly code faithfully implements the dataflow semantics of source programs.
We resolve two key technical challenges. The first is the change from a synchronous dataflow semantics, where programs manipulate streams of values, to an imperative one, where computations manipulate memory sequentially. The second is the verified compilation of an imperative language with encapsulated state to C~code where the state is realized by nested records. We also treat a standard control optimization that eliminates unnecessary conditional statements.
Tue 20 Jun
|16:10 - 16:35|
Timothy BourkeINRIA, Lélio BrunENS/Inria, Pierre-Evariste DagandLIP6/CNRS , Xavier LeroyInria, Marc PouzetÉcole normale supérieure, Lionel RiegCollège de FranceMedia Attached
|16:35 - 17:00|
Parosh Aziz AbdullaUppsala University, Sweden, Mohamed Faouzi AtigUppsala University, Phi-Diep BuiUppsala University, Yu-Fang Chen, Lukas Holik, Ahmed Rezine, Philipp RuemmerUppsala UniversityMedia Attached