REMS-DeepSpec 2020 provides a forum for researchers interested in foundational specifications and rigorous engineering of mainstream systems and their components. It will consist of in-depth presentations by members of the REMS project (UK) and DeepSpec (US), invited talks by external experts, and general talks selected in response to a call for short abstracts. No formal proceedings are associated with this event.
The workshop brings together two large projects, REMS and DeepSpec. REMS aims to develop semantics and rigorous engineering methods that apply to mainstream systems, and DeepSpec to push forward the state of the art in applying computer proof assistants to verify realistic software and hardware stacks at scale.
Talks
Call for Papers
Presentations will be selected based on one or two-page abstracts, which must be in PDF format.
Dates
Mon 15 JunDisplayed time zone: Pacific Time (US & Canada) change
Mon 15 Jun
Displayed time zone: Pacific Time (US & Canada) change
05:00 - 07:00 | |||
05:00 15mTalk | Welcome and brief project overviews REMS-DeepSpec File Attached | ||
05:15 40mTalk | Verifying Crash-Safe, Concurrent Systems with Perennial REMS-DeepSpec Joseph Tassarotti Boston College | ||
06:05 40mTalk | Compositional Atomic Distributed Object Specifications for Distributed System Verification REMS-DeepSpec Ji-Yong Shin Yale University | ||
07:00 - 09:00 | |||
07:00 40mTalk | Sail: ISA semantics, symbolic execution, and axiomatic concurrency for ARMv8-A and RISC-V REMS-DeepSpec P: Alasdair Armstrong University of Cambridge, Thomas Bauereiss University of Cambridge, Brian Campbell University of Edinburgh, Alastair Reid Google Research, Kathryn E. Gray Facebook, Robert M. Norton University of Cambridge, Prashanth Mundkur SRI International, Mark Wassell University of Cambridge, Jon French University of Cambridge, Christopher Pulte University of Cambridge, UK, Shaked Flur Google, Ian Stark The University of Edinburgh, Neel Krishnaswami Computer Laboratory, University of Cambridge, Peter Sewell University of Cambridge | ||
07:50 40mTalk | ARMv8 and RISC-V relaxed memory concurrency REMS-DeepSpec P: Shaked Flur Google, P: Christopher Pulte University of Cambridge, UK, Luc Maranget Inria Paris, Will Deacon ARM Ltd., Susmit Sarkar University of St. Andrews, Ben Simner , Jean Pichon-Pharabod University of Cambridge, UK, Jeehoon Kang KAIST, Sung-Hwan Lee Seoul National University, South Korea, Chung-Kil Hur Seoul National University, South Korea, Alasdair Armstrong University of Cambridge, Ohad Kammar University of Edinburgh, Jon French University of Cambridge, Kathryn E. Gray Facebook, Ali Sezgin University of Cambridge, Peter Sewell University of Cambridge File Attached | ||
09:00 - 11:00 | |||
09:00 40mTalk | Cerberus: executable reference semantics and memory object models for ISO and de facto C REMS-DeepSpec P: Kayvan Memarian University of Cambridge, Victor B. F. Gomes University of Cambridge, UK, Stella Lau , Jean Pichon-Pharabod University of Cambridge, UK, Justus Matthiesen University of Cambridge, Peter Sewell University of Cambridge | ||
09:50 40mTalk | Verified Software Toolchain: a powerful and practical tool REMS-DeepSpec Andrew W. Appel Princeton | ||
Tue 16 JunDisplayed time zone: Pacific Time (US & Canada) change
Tue 16 Jun
Displayed time zone: Pacific Time (US & Canada) change
05:00 - 07:00 | |||
05:00 40mTalk | Rigorous modelling and proof for system security engineering: verifying whole-ISA security properties of CHERI-{MIPS,RISC-V,ARM} REMS-DeepSpec Thomas Bauereiss University of Cambridge, Kyndylan Nienhuis University of Cambridge, Alexandre Joannou University of Cambridge, Anthony Fox University of Cambridge, UK, Michael Roe University of Cambridge, Brian Campbell University of Edinburgh, Matthew Naylor University of Cambridge, Robert M. Norton University of Cambridge, Simon W. Moore University of Cambridge, Peter G. Neumann SRI International, Ian Stark The University of Edinburgh, Robert N. M. Watson University of Cambridge, Peter Sewell University of Cambridge File Attached | ||
05:50 40mTalk | Katamaran: semi-automated verification of ISA specifications REMS-DeepSpec Steven Keuchel , Georgy Lukyanov Newcastle University, UK, Dominique Devriese Vrije Universiteit Brussel File Attached | ||
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 | ||
09:00 - 11:00 | |||
09:00 40mTalk | Representing recursive and impure programs in Coq: from a toy assembly language to a modular formal semantics for LLVM IR REMS-DeepSpec Yannick Zakowski University of Pennsylvania | ||
09:50 40mTalk | The Verified IoT Lightbulb: Connecting Hardware and Software in a Simple Embedded System REMS-DeepSpec Adam Chlipala Massachusetts Institute of Technology, Andres Erbsen , Samuel Gruetter Massachusetts Institute of Technology, Joonwon Choi Massachusetts Institute of Technology, USA | ||
Important Dates AoE (UTC-12h)
| Mon 15 - Tue 16 Jun 2020 Workshop |
| Fri 24 Apr 2020 Notification |
| Tue 31 Mar 2020 Submission Deadline |
Submission Link
