Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Toggle navigation
Attending
Venue: Online!
Statement on Current Events
Registration
Code of Conduct
Sponsorship
Student participation and support
Video recording
Program
Complete Program
Your Program
Mon 15 Jun
Tue 16 Jun
Wed 17 Jun
Thu 18 Jun
Fri 19 Jun
Tracks
PLDI 2020
Ask Me Anything
SIGPLAN CARES
Sponsors
PLDI Research Papers
PLDI Research Artifacts
Student Research Competition
Tutorials
- Declarative Language Definition with Spoofax
- Design Space Exploration
- Programming Quantum Computers: A Primer with IBM Q and D-Wave Exercises
- Programming for Autonomy
Student Volunteering
Co-hosted Conferences
ISMM
ISMM
ISMM
LCTES
Co-hosted Events
Ally Skills@PLDI
(Cancelled)
Workshops
ARRAY
(Cancelled)
BAPL
(Cancelled)
Infer Practitioners
MAPL
PLMW@PLDI
REMS-DeepSpec
SOAP
Organization
PLDI 2020 Committees
Organizing Committee
Steering Committee
Track Committees
PLDI Research Papers
Program Committee
External Program Committee
External Review Committee
PLDI Research Artifacts
Student Research Competition
Student Volunteering
Contributors
People Index
Co-hosted Conferences
ISMM
Organizing Committee
Program Committee
External Review Committee
Steering Committee
LCTES
Organizing Committee
Program Committee
Co-hosted Events
Ally Skills@PLDI
Organizing Committee
Workshops
ARRAY
Organizing Committee
Program Committee
BAPL
Organizing Committee
Program Committee
External Review Committee
Infer Practitioners
Organizing Committee
Program Committee
MAPL
Organizing Committee
Program Committee
PLMW@PLDI
Organizing Committee
REMS-DeepSpec
Organizing Committee
Program Committee
SOAP
Keynote Speakers
Organizing Committee
Program Committee
Search
Series
Series
PLDI 2025
PLDI 2024
PLDI 2023
PLDI 2022
PLDI 2021
PLDI 2020
PLDI 2019
PLDI 2018
PLDI 2017
PLDI 2016
PLDI 2015
Sign in
Sign up
PLDI 2020
(
series
) /
Online!
/
Room information: REMS/DeepSpec live stream
Venue
Online!
Room name
REMS/DeepSpec live stream
Floor
0
Room Information
Slack channel:
#rems-deepspec
YouTube live streams:
Monday 15 June
Tuedsay 16 June
Program
Detailed Table
Session Timeline
Detailed Timeline
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT-07:00) Pacific Time (US & Canada)
.
Use conference time zone: (GMT-07:00) Pacific Time (US & Canada)
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-09:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-08:00) Alaska
(GMT-07:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-07:00) Pacific Time (US & Canada)
(GMT-06:00) Mountain Time (US & Canada)
(GMT-06:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-06:00) Easter Island
(GMT-05:00) Central Time (US & Canada)
(GMT-04:00) Eastern Time (US & Canada)
(GMT-04:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-04:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-03:00) Atlantic Time (Goose Bay)
(GMT-03:00) Atlantic Time (Canada)
(GMT-02:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-02:00) Miquelon, St. Pierre
(GMT-02:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT) Azores
(UTC) Coordinated Universal Time
(GMT+01:00) Belfast
(GMT+01:00) Dublin
(GMT+01:00) Lisbon
(GMT+01:00) London
(GMT) Monrovia, Reykjavik
(GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+02:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+03:00) Athens
(GMT+03:00) Beirut
(GMT+02:00) Cairo
(GMT+03:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+03:00) Jerusalem
(GMT+03:00) Minsk
(GMT+03:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+04:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+09:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+10:00) Hobart
(GMT+10:00) Vladivostok
(GMT+10:30) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+11:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+12:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+12:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
The GMT offsets shown reflect the offsets
at the moment of the conference
.
Time Band
By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.
Display full program
Specify a time band
-
Save
×
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 1
REMS-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 2
REMS-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 3
REMS-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 4
REMS-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 5
REMS-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 6
REMS-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
Room
5:00
30
6:00
30
7:00
30
8:00
30
9:00
30
10:00
30
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
Room
5:00
30
6:00
30
7:00
30
8:00
30
9:00
30
10:00
30
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
Room
5:00
15
30
45
6:00
15
30
45
7:00
15
30
45
8:00
15
30
45
9:00
15
30
45
10:00
15
30
45
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
Room
5:00
15
30
45
6:00
15
30
45
7:00
15
30
45
8:00
15
30
45
9:00
15
30
45
10:00
15
30
45
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
x
Sun 8 Sep 02:27