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
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:10 - 17:00: Verified ComputationPLDI Research Papers at Aula Master
Chair(s): Alvin CheungUniversity of Washington
16:10 - 16:35
A Formally Verified Compiler for Lustre
PLDI Research Papers
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
16:35 - 17:00
Flatten and Conquer (A Framework for Efficient Analysis of String Constraints)
PLDI Research Papers
Parosh Aziz AbdullaUppsala University, Sweden, Mohamed Faouzi AtigUppsala University, Bui Phi DiepUppsala University, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp RuemmerUppsala University
Media Attached