Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020

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

Title
Cerberus: executable reference semantics and memory object models for ISO and de facto C
REMS-DeepSpec
Compositional Atomic Distributed Object Specifications for Distributed System Verification
REMS-DeepSpec
Representing recursive and impure programs in Coq: from a toy assembly language to a modular formal semantics for LLVM IR
REMS-DeepSpec
The Verified IoT Lightbulb: Connecting Hardware and Software in a Simple Embedded System
REMS-DeepSpec
WebAssembly: sequential and concurrent semantics
REMS-DeepSpec
ARMv8 and RISC-V relaxed memory concurrency
REMS-DeepSpec
File Attached
Gillian: a Multi-language Platform for Program Correctness and Incorrectness
REMS-DeepSpec
Katamaran: semi-automated verification of ISA specifications
REMS-DeepSpec
File Attached
Rigorous modelling and proof for system security engineering: verifying whole-ISA security properties of CHERI-{MIPS,RISC-V,ARM}
REMS-DeepSpec
File Attached
Sail: ISA semantics, symbolic execution, and axiomatic concurrency for ARMv8-A and RISC-V
REMS-DeepSpec
Verified Software Toolchain: a powerful and practical tool
REMS-DeepSpec
Verifying Crash-Safe, Concurrent Systems with Perennial
REMS-DeepSpec
Welcome and brief project overviews
REMS-DeepSpec
File Attached

Call for Papers

Presentations will be selected based on one or two-page abstracts, which must be in PDF format.

Dates
You're viewing the program in a time zone which is different from your device's time zone - change time zone

Mon 15 Jun

Displayed time zone: Pacific Time (US & Canada) change

07:00 - 09:00
REMS-DeepSpec Session 2REMS-DeepSpec at REMS/DeepSpec live stream
07:00
40m
Talk
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
40m
Talk
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
REM-DeepSpec Session 3REMS-DeepSpec at REMS/DeepSpec live stream
09:00
40m
Talk
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
40m
Talk
Verified Software Toolchain: a powerful and practical tool
REMS-DeepSpec
Andrew Appel Princeton

Tue 16 Jun

Displayed time zone: Pacific Time (US & Canada) change

05:00 - 07:00
REMS-DeepSpec Session 4REMS-DeepSpec at REMS/DeepSpec live stream
05:00
40m
Talk
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
40m
Talk
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
REMS-DeepSpec Session 5REMS-DeepSpec at REMS/DeepSpec live stream
07:00
40m
Talk
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
40m
Talk
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, Rao Xiaoj Imperial College
09:00 - 11:00
REMS-DeepSpec Session 6REMS-DeepSpec at REMS/DeepSpec live stream
09:00
40m
Talk
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
40m
Talk
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