Write a Blog >>
Fri 24 Jan 2020 16:18 - 16:40 at Ile de France III (IDF III) - Verified & Secure Compilation Chair(s): Andrew Appel

Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications. Tools like SCADE Suite and Simulink/Stateflow are equipped with compilers to translate such specifications into executable code. They provide programming languages for composing functions over streams as typified by Dataflow Synchronous Languages like Lustre.

Recent work builds on CompCert to specify and verify a compiler for the core of Lustre in the Coq Interactive Theorem Prover. It formally links the stream-based semantics of the source language to the sequential memory manipulations of generated assembly code. We extend this work to treat a primitive for resetting subsystems. Our contributions include new semantic rules that are suitable for mechanized reasoning, a novel intermediate language for generating optimized code, and proofs of correctness for the associated compilation passes.

Slides (slides.pdf)472KiB

Fri 24 Jan
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

15:35 - 16:40: Research Papers - Verified & Secure Compilation at Ile de France III (IDF III)
Chair(s): Andrew AppelPrinceton
POPL-2020-Research-Papers15:35 - 15:56
Gilles BartheMPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Sandrine BlazyUniv Rennes- IRISA, Benjamin GregoireINRIA, Rémi HutinIRISA / ENS Rennes, Vincent LaporteInria, David PichardieUniv Rennes, ENS Rennes, IRISA, Alix TrieuAarhus University
Link to publication DOI Media Attached File Attached
POPL-2020-Research-Papers15:56 - 16:18
Youngju SongSeoul National University, Minki ChoSeoul National University, Dongjoo KimSeoul National University, Yonghyun KimSeoul National University, South Korea, Jeehoon KangKAIST, Chung-Kil HurSeoul National University
Link to publication DOI Media Attached File Attached
POPL-2020-Research-Papers16:18 - 16:40
Timothy BourkeInria / École normale supérieure, Lélio BrunENS/Inria, Marc PouzetÉcole normale supérieure
Link to publication DOI Media Attached File Attached