Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Mon 18 Oct 2021 09:10 - 10:10 at Zurich G - Welcome to REBLS & Keynote Chair(s): Louis Mandel

Embedded control systems have long been designed using block diagrams and state machines. These models often simply guide the manual implementation of software. But in Model-Based Design they are treated as programs and compiled automatically into low-level code. This is the approach taken in academic languages like Lustre and commercial tools like Simulink and SCADE Suite.

This talk presents results from the ongoing Vélus project that aims to specify a compiler for Model-Based Design (Lustre with features from Scade 6) in an Interactive Theorem Prover (Coq). It will describe the model of synchronous streams that gives a semantics to the input language and features of the proof that links this model to the step-by-step model of the generated assembly code. Our prototype builds on the CompCert C compiler and we will talk about some of the challenges of interfacing with such a low-level model of the underlying machine.

Mon 18 Oct

Displayed time zone: Central Time (US & Canada) change

09:00 - 10:20
Welcome to REBLS & KeynoteREBLS at Zurich G
Chair(s): Louis Mandel IBM Research
Day opening
Welcome to REBLS
Louis Mandel IBM Research
Specification and End-to-End Proof of a Reactive Language and Its Compiler (Invited Talk)Keynote