Implementing reliable distributed systems is challenging because such systems must tolerate faults gracefully: machines may crash and networks may reorder, drop, or duplicate packets. Bugs in these systems can lead to loss of critical data and unacceptable service outages.
We present Verdi, a framework for implementing and formally verifying practical distributed systems in Coq. Verdi formalizes various 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 and a primary-backup replication mechanism.
[ bib | publisher | project | slides | paper ] Back
This file was generated by bibtex2html 1.98.