BAPL 2020
Dates to be announced
co-located with PLDI 2020
PLDI 2020 (series) / BAPL 2020 (series) / Online! /

Room information: REMS/DeepSpec live stream

VenueOnline!
Room nameREMS/DeepSpec live stream
Floor0
Room Information

Slack channel: #rems-deepspec

YouTube live streams:

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

05:00 - 07:00
REMS-DeepSpec Session 1REMS-DeepSpec at REMS/DeepSpec live stream
05:00
15m
Talk
Welcome and brief project overviews
REMS-DeepSpec
Peter Sewell University of Cambridge, Lennart Beringer Princeton University
File Attached
05:15
40m
Talk
Verifying Crash-Safe, Concurrent Systems with Perennial
REMS-DeepSpec
Joseph Tassarotti Boston College
06:05
40m
Talk
 Compositional Atomic Distributed Object Specifications for Distributed System Verification
REMS-DeepSpec
Ji-Yong Shin Yale University
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 W. 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, Xiaojia Rao 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

Mon 15 Jun

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

Room5:00306:00307:00308:00309:003010:0030
REMS/DeepSpec live stream

REMS-DeepSpec

REMS-DeepSpec Session 1

REMS-DeepSpec

REMS-DeepSpec Session 2

REMS-DeepSpec

REM-DeepSpec Session 3

Tue 16 Jun

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

Room5:00306:00307:00308:00309:003010:0030
REMS/DeepSpec live stream

REMS-DeepSpec

REMS-DeepSpec Session 4

REMS-DeepSpec

REMS-DeepSpec Session 5

REMS-DeepSpec

REMS-DeepSpec Session 6

Mon 15 Jun

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

Room5:001530456:001530457:001530458:001530459:0015304510:00153045
REMS/DeepSpec live stream
REMS-DeepSpec
Welcome and brief project overviews
05:00 - 05:15
REMS-DeepSpec
Verifying Crash-Safe, Concurrent Systems with Perennial
05:15 - 05:55
REMS-DeepSpec
Compositional Atomic Distributed Object Specifications for Distributed ...
06:05 - 06:45
REMS-DeepSpec
Sail: ISA semantics, symbolic execution, and axiomatic concurrency for ...
07:00 - 07:40
REMS-DeepSpec
ARMv8 and RISC-V relaxed memory concurrency
07:50 - 08:30
REMS-DeepSpec
Cerberus: executable reference semantics and memory object models for ...
09:00 - 09:40
REMS-DeepSpec
Verified Software Toolchain: a powerful and practical tool
09:50 - 10:30

Tue 16 Jun

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

Room5:001530456:001530457:001530458:001530459:0015304510:00153045
REMS/DeepSpec live stream
REMS-DeepSpec
Rigorous modelling and proof for system security engineering: verifying ...
05:00 - 05:40
REMS-DeepSpec
Katamaran: semi-automated verification of ISA specifications
05:50 - 06:30
REMS-DeepSpec
Gillian: a Multi-language Platform for Program Correctness and Incorrec ...
07:00 - 07:40
REMS-DeepSpec
WebAssembly: sequential and concurrent semantics
07:50 - 08:30
REMS-DeepSpec
Representing recursive and impure programs in Coq: from a toy assembly ...
09:00 - 09:40
REMS-DeepSpec
The Verified IoT Lightbulb: Connecting Hardware and Software in a Simp ...
09:50 - 10:30