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

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