Write a Blog >>
Tue 20 Jun 2017 16:10 - 16:35 at Aula Master - Verified Computation Chair(s): Alvin Cheung

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

pldi-2017-papers
16:10 - 17:00: PLDI Research Papers - Verified Computation at Aula Master
Chair(s): Alvin CheungUniversity of Washington
pldi-2017-papers149796780000016:10 - 16:35
Talk
Timothy BourkeINRIA, Lélio BrunENS/Inria, Pierre-Evariste DagandLIP6/CNRS , Xavier LeroyInria, Marc PouzetÉcole normale supérieure, Lionel RiegCollège de France
Media Attached
pldi-2017-papers149796930000016:35 - 17:00
Talk
Parosh Aziz AbdullaUppsala University, Sweden, Mohamed Faouzi AtigUppsala University, Phi-Diep BuiUppsala University, Yu-Fang Chen, Lukas Holik, Ahmed Rezine, Philipp RuemmerUppsala University
Media Attached