Verifying Crash-Safe, Concurrent Systems with Perennial
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 - 05:15|
|05:15 - 05:55|
Joseph TassarottiBoston College
|06:05 - 06:45|
Ji-Yong ShinYale University