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

Dates
Rooms
Tracks
Badges
Your Program
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