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

Conference Day
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 ArmstrongUniversity of Cambridge, Thomas BauereissUniversity of Cambridge, Brian CampbellUniversity of Edinburgh, Alastair ReidGoogle Research, Kathryn E. GrayFacebook, Robert M. NortonUniversity of Cambridge, Prashanth MundkurSRI International, Mark WassellUniversity of Cambridge, Jon FrenchUniversity of Cambridge, Christopher PulteUniversity of Cambridge, UK, Shaked FlurGoogle, Ian StarkThe University of Edinburgh, Neel KrishnaswamiComputer Laboratory, University of Cambridge, Peter SewellUniversity of Cambridge
07:50
40m
Talk
ARMv8 and RISC-V relaxed memory concurrency
REMS-DeepSpec
P: Shaked FlurGoogle, P: Christopher PulteUniversity of Cambridge, UK, Luc MarangetInria Paris, Will DeaconARM Ltd., Susmit SarkarUniversity of St. Andrews, Ben Simner, Jean Pichon-PharabodUniversity of Cambridge, UK, Jeehoon KangKAIST, Sung-Hwan LeeSeoul National University, South Korea, Chung-Kil HurSeoul National University, South Korea, Alasdair ArmstrongUniversity of Cambridge, Ohad KammarUniversity of Edinburgh, Jon FrenchUniversity of Cambridge, Kathryn E. GrayFacebook, Ali SezginUniversity of Cambridge, Peter SewellUniversity 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 MemarianUniversity of Cambridge, Victor B. F. GomesUniversity of Cambridge, UK, Stella Lau, Jean Pichon-PharabodUniversity of Cambridge, UK, Justus MatthiesenUniversity of Cambridge, Peter SewellUniversity of Cambridge
09:50
40m
Talk
Verified Software Toolchain: a powerful and practical tool
REMS-DeepSpec
Andrew AppelPrinceton

Conference Day
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 BauereissUniversity of Cambridge, Kyndylan NienhuisUniversity of Cambridge, Alexandre JoannouUniversity of Cambridge, Anthony FoxUniversity of Cambridge, UK, Michael RoeUniversity of Cambridge, Brian CampbellUniversity of Edinburgh, Matthew NaylorUniversity of Cambridge, Robert M. NortonUniversity of Cambridge, Simon W. MooreUniversity of Cambridge, Peter G. NeumannSRI International, Ian StarkThe University of Edinburgh, Robert N. M. WatsonUniversity of Cambridge, Peter SewellUniversity of Cambridge
File Attached
05:50
40m
Talk
Katamaran: semi-automated verification of ISA specifications
REMS-DeepSpec
Steven Keuchel, Georgy LukyanovNewcastle University, UK, Dominique DevrieseVrije 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 GardnerImperial College London, UK, José Fragoso SantosImperial College London, Petar MaksimovićImperial College London, UK, Sacha-Élie AyounImperial College London, UK
07:50
40m
Talk
WebAssembly: sequential and concurrent semantics
REMS-DeepSpec
P: Conrad WattUniversity of Cambridge, UK, Guillaume BarbierENS Rennes, France, Martin BodinImperial College London, Sunjay CauligiUniversity of California at San Diego, USA, Craig DisselkoenUniversity of California at San Diego, USA, Stephen DolanUniversity of Cambridge, UK, Shaked FlurGoogle, Philippa GardnerImperial College London, UK, Tal GarfinkelStanford University, Shu-yu GuoBloomberg, USA, Neel KrishnaswamiComputer Laboratory, University of Cambridge, Amit Levy, Petar MaksimovićImperial College London, UK, Jean Pichon-PharabodUniversity of Cambridge, UK, Anton PodkopaevMPI-SWS, NRU HSE, JetBrains Research, Natalie PopescuUniversity of California San Diego, Christopher PulteUniversity of Cambridge, UK, John RennerUniversity of California at San Diego, USA, Andreas RossbergDfinity Stiftung, Deian StefanUniversity of California at San Diego, USA, Rao XiaojImperial 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 ZakowskiUniversity of Pennsylvania
09:50
40m
Talk
The Verified IoT Lightbulb: Connecting Hardware and Software in a Simple Embedded System
REMS-DeepSpec
Adam ChlipalaMassachusetts Institute of Technology, Andres Erbsen, Samuel GruetterMassachusetts Institute of Technology, Joonwon ChoiMassachusetts Institute of Technology, USA