Write a Blog >>

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

Displayed time zone: Saskatchewan, Central America change

15:35 - 16:40
Verified & Secure CompilationResearch Papers at Ile de France III (IDF III)
Chair(s): Andrew W. Appel Princeton
15:35
21m
Talk
Formal Verification of a Constant-Time Preserving C Compiler
Research Papers
Gilles Barthe MPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Sandrine Blazy Univ Rennes- IRISA, Benjamin Gregoire INRIA, Rémi Hutin IRISA / ENS Rennes, Vincent Laporte Inria, David Pichardie Univ Rennes, ENS Rennes, IRISA, Alix Trieu Aarhus University
Link to publication DOI Media Attached File Attached
15:56
21m
Talk
CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification
Research Papers
Youngju Song Seoul National University, Minki Cho Seoul National University, Dongjoo Kim Seoul National University, Yonghyun Kim Seoul National University, South Korea, Jeehoon Kang KAIST, Chung-Kil Hur Seoul National University
Link to publication DOI Media Attached File Attached
16:18
21m
Talk
Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset
Research Papers
Timothy Bourke Inria / École normale supérieure, Lelio Brun ENS/Inria, Marc Pouzet École normale supérieure
Link to publication DOI Media Attached File Attached