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 JanDisplayed time zone: Belfast change
16:37 - 17:43 | Verified Compilation and ConcurrencyResearch Papers at Sala I Chair(s): Michael Greenberg Pomona College | ||
16:37 22mTalk | A Calculus for Esterel: If can, can. If no can, no can. Research Papers Spencer P. Florence Northwestern University, USA, Shu-Hung You Northwestern University, USA, Jesse A. Tov Northwestern University, Department of Electrical Engineering and Computer Science, Robby Findler Northwestern University, USA Link to publication DOI Media Attached File Attached | ||
16:59 22mTalk | An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code Research Papers Link to publication DOI Media Attached File Attached | ||
17:21 22mTalk | A Verified, Efficient Embedding of a Verifiable Assembly Language Research Papers Aymeric Fromherz Carnegie Mellon University, Nick Giannarakis Princeton University, Chris Hawblitzel Microsoft Research, Bryan Parno , Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research Link to publication DOI Media Attached File Attached |