WebAssembly: sequential and concurrent semantics
joint work with Guillaume Barbier, Martin Bodin, Sunjay Cauligi, Craig Disselkoen, Stephen Dolan, Shaked Flur, Philippa Gardner, Tal Garfinkel, Shu-yu Guo, Neelakantan R. Krishnaswami, Amit Levy, Petar Maksimović, Jean Pichon-Pharabod, Anton Podkopaev, Natalie Popescu, Christopher Pulte, John Renner, Andreas Rossberg, Deian Stefan, Rao Xiaoj
WebAssembly is the first new programming language to be natively supported on the Web platform since JavaScript. WebAssembly was designed from the ground up using formal semantics, and each new feature must be fully formally specified before it can be adopted into the standard. This talk will describe recent work in mechanising WebAssembly’s semantics, and specifying the language’s relaxed memory model. We will also discuss future challenges in verifying security-related properties of the language.
Tue 16 JunDisplayed time zone: Pacific Time (US & Canada) change
07:00 - 09:00 | |||
07:00 40mTalk | Gillian: a Multi-language Platform for Program Correctness and Incorrectness REMS-DeepSpec Philippa Gardner Imperial College London, UK, José Fragoso Santos Imperial College London, Petar Maksimović Imperial College London, UK, Sacha-Élie Ayoun Imperial College London, UK | ||
07:50 40mTalk | WebAssembly: sequential and concurrent semantics REMS-DeepSpec P: Conrad Watt University of Cambridge, UK, Guillaume Barbier ENS Rennes, France, Martin Bodin Imperial College London, Sunjay Cauligi University of California at San Diego, USA, Craig Disselkoen University of California at San Diego, USA, Stephen Dolan University of Cambridge, UK, Shaked Flur Google, Philippa Gardner Imperial College London, UK, Tal Garfinkel Stanford University, Shu-yu Guo Bloomberg, USA, Neel Krishnaswami Computer Laboratory, University of Cambridge, Amit Levy , Petar Maksimović Imperial College London, UK, Jean Pichon-Pharabod University of Cambridge, UK, Anton Podkopaev MPI-SWS, NRU HSE, JetBrains Research, Natalie Popescu University of California San Diego, Christopher Pulte University of Cambridge, UK, John Renner University of California at San Diego, USA, Andreas Rossberg Dfinity Stiftung, Deian Stefan University of California at San Diego, USA, Xiaojia Rao Imperial College | ||