Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Mon 15 Jun 2020 05:15 - 05:55 at REMS/DeepSpec live stream - REMS-DeepSpec Session 1

Proving that concurrent systems are crash-safe is challenging because non-determinism arising from concurrency and crashes interact in subtle ways. Perennial is a framework for verifying these systems that is built on top of the Iris concurrency framework. Handling crashes requires reexamining principles about invariants and ownership of resources that underlie Concurrent Separation Logics like Iris. After explaining the core concepts in Perennial, I will describe on-going work improving and using Perennial to verify larger systems.

Mon 15 Jun
Times are displayed in time zone: (GMT-07:00) Pacific Time (US & Canada) change

05:00 - 07:00: REMS-DeepSpec 2020 - REMS-DeepSpec Session 1 at REMS/DeepSpec live stream
rems-deepspec-202005:00 - 05:15
Peter SewellUniversity of Cambridge, Lennart BeringerPrinceton University
File Attached
rems-deepspec-202005:15 - 05:55
Joseph TassarottiBoston College
rems-deepspec-202006:05 - 06:45
Ji-Yong ShinYale University