Tue 16 Jun 2015 15:15 - 15:40 at PLDI Main RED (Portland 256) - Semantics I Chair(s): Hans-J. Boehm

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.

PLDI 2015 Artifact Evaluated Badge

Tue 16 Jun

Displayed time zone: Tijuana, Baja California change

14:00 - 15:40
14:00
25m
Talk
A Formal C Memory Model Supporting Integer-Pointer Casts
Research Papers
Jeehoon Kang Seoul National University, Chung-Kil Hur Seoul National University, William Mansky University of Pennsylvania, Dmitri Garbuzov University of Pennsylvania, Steve Zdancewic , Viktor Vafeiadis MPI-SWS, Germany
Media Attached
14:25
25m
Talk
Defining the undefinedness of C
Research Papers
Chris Hathhorn University of Missouri, Chucky Ellison University of Illinois, Grigore Roşu University of Illinois at Urbana-Champaign
Media Attached
14:50
25m
Talk
KJS: A Complete Formal Semantics of JavaScript
Research Papers
Daejun Park University of Illinois at Urbana-Champaign, Andrei Stefanescu University of Illinois at Urbana-Champaign, Grigore Roşu University of Illinois at Urbana-Champaign
Media Attached
15:15
25m
Talk
Verdi: A Framework for Formally Verifying Distributed System Implementations
Research Papers
James R. Wilcox University of Washington, Doug Woos University of Washington, Pavel Panchekha University of Washington, Zachary Tatlock University of Washington, Seattle, Xi Wang University of Washington, Michael D. Ernst University of Washington, Thomas Anderson University of Washington
Media Attached