Download: PDF, slides (PDF), Verdi website, Verdi implementation.
“Verdi: A framework for implementing and formally verifying distributed systems” by James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson. In PLDI 2015: Proceedings of the ACM SIGPLAN 2015 Conference on Programming Language Design and Implementation, (Portland, OR, USA), June 2015, pp. 357-368.
Distributed systems are difficult to implement correctly because they must handle both concurrency and failures: machines may crash at arbitrary points and networks may reorder, drop, or duplicate packets. Further, their behavior is often too complex to permit exhaustive testing. Bugs in these systems have led to the loss of critical data and unacceptable service outages.
We present Verdi, a framework for implementing and formally verifying distributed systems in Coq. Verdi formalizes various network semantics with different faults, and the developer chooses the most appropriate fault model when verifying their implementation. Furthermore, Verdi eases the verification burden by enabling the developer to first verify their system under 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 the first mechanically checked proof of linearizability of the Raft state machine replication algorithm, as well as verified implementations of a primary-backup replication system and a key-value store. These verified systems provide similar performance to unverified equivalents.
Download: PDF, slides (PDF), Verdi website, Verdi implementation.
BibTeX entry:
@inproceedings{WilcoxWPTWEA2015,
author = {James R. Wilcox and Doug Woos and Pavel Panchekha and Zachary
Tatlock and Xi Wang and Michael D. Ernst and Thomas Anderson},
title = {Verdi: A framework for implementing and formally verifying
distributed systems},
booktitle = {PLDI 2015: Proceedings of the {ACM} {SIGPLAN} 2015
Conference on Programming Language Design and Implementation},
pages = {357--368},
address = {Portland, OR, USA},
month = jun,
year = {2015}
}
(This webpage was created with bibtex2web.)
Back to Michael Ernst's publications.