Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Fri 18 Jan 2019 16:37 - 16:59 at Sala I - Verified Compilation and Concurrency Chair(s): Michael Greenberg

The language Esterel has found success in many safety-critical applications, such as fly-by-wire systems and nuclear power plant control software. Its imperative style is natural to programmers building such systems and its precise semantics makes it work well for reasoning about programs.

Existing semantics of Esterel generally fall into two categories: translation to Boolean circuits, or operational semantics that give a procedure for running a whole program. In contrast, equational theories enable reasoning about program behavior via equational rewrites at the source level. Such theories form the basis for proofs of transformations inside compilers or for program refactorings, and defining program evaluation syntactically.

This paper presents the first such equational calculus for Esterel. It also illustrates the calculus’s usefulness with a series of example equivalences and discuss how it enabled us to find bugs in Esterel implementations.

Slides (talk.pdf)2.90MiB

Fri 18 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

16:37 - 17:43: Verified Compilation and ConcurrencyResearch Papers at Sala I
Chair(s): Michael GreenbergPomona College
16:37 - 16:59
A Calculus for Esterel: If can, can. If no can, no can.
Research Papers
Spencer P. FlorenceNorthwestern University, USA, Shu-Hung YouNorthwestern University, USA, Jesse A. TovNorthwestern University, Department of Electrical Engineering and Computer Science, Robby FindlerNorthwestern University, USA
Link to publication DOI Media Attached File Attached
16:59 - 17:21
An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code
Research Papers
Yuting WangYale University, Pierre WilkeYale University, Zhong ShaoYale University
Link to publication DOI Media Attached File Attached
17:21 - 17:43
A Verified, Efficient Embedding of a Verifiable Assembly Language
Research Papers
Aymeric FromherzCarnegie Mellon University, Nick GiannarakisPrinceton University, Chris HawblitzelMicrosoft Research, Bryan Parno, Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research
Link to publication DOI Media Attached File Attached