Verdi: A Framework for Formally Verifying Distributed System Implementations
Implementing reliable distributed systems is challenging because they run in unreliable environments and must tolerate faults gracefully: machines may crash and networks may reorder, drop, or duplicate packets. Failing to do so can lead to catastrophic failures and major outage of web services.
We present Verdi, a framework for implementing and formally verifying practical distributed systems in Coq. Verdi formalizes five network semantics with different kinds of faults, and allows developers to choose the most appropriate fault model when verifying their implementation. Furthermore, Verdi eases the verification burden by enabling developers to construct systems from modular components. This separation of concerns eases reasoning because the developer can verify their system in an idealized fault model, then transfer the resulting correctness guarantees to a more realistic fault model without any additional proof burden. To demonstrate Verdi’s utility, we present a series of case studies including a key-value store application and a primary-backup replication mechanism.
Tue 16 Jun Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change
|14:00 - 14:25|
Jeehoon KangSeoul National University, Chung-Kil HurSeoul National University, William ManskyUniversity of Pennsylvania, Dmitri GarbuzovUniversity of Pennsylvania, Steve Zdancewic, Viktor VafeiadisMPI-SWS, GermanyMedia Attached
|14:25 - 14:50|
Chris HathhornUniversity of Missouri, Chucky EllisonUniversity of Illinois, Grigore RosuUniversity of Illinois at Urbana-ChampaignMedia Attached
|14:50 - 15:15|
Daejun ParkUniversity of Illinois at Urbana-Champaign, Andrei StefanescuUniversity of Illinois at Urbana-Champaign, Grigore RosuUniversity of Illinois at Urbana-ChampaignMedia Attached
|15:15 - 15:40|
James R. WilcoxUniversity of Washington, Doug WoosUniversity of Washington, Pavel PanchekhaUniversity of Washington, Zachary Tatlock, Xi WangUniversity of Washington, Michael D. ErnstUniversity of Washington, Thomas AndersonUniversity of WashingtonMedia Attached