SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Wed 20 Oct 2021 08:25 - 08:40 at Zurich B - Distributed Programming - mirror Chair(s): Shigeru Chiba
Wed 20 Oct 2021 16:25 - 16:40 at Zurich B - Distributed Programming Chair(s): Mohsen Lesani

The last decade has sparked several valiant efforts in deductive verification of distributed agreement protocols such as consensus and leader election. Oddly, there have been far fewer verification efforts that go beyond the core protocols and target applications that are built on top of agreement protocols. This is unfortunate, as agreement-based distributed services such as data stores, locks, and ledgers are ubiquitous and potentially permit modular, scalable verification approaches that mimic their modular design.

We address this need for verification of distributed agreement-based systems through our novel modeling and verification framework, QuickSilver, that is not only modular, but also fully automated. The key enabling feature of QuickSilver is our encoding of abstractions of verified agreement protocols that facilitates modular, decidable, and scalable automated verification. We demonstrate the potential of QuickSilver by modeling and efficiently verifying a series of tricky case studies, adapted from real-world applications, such as a data store, a lock service, a surveillance system, a pathfinding algorithm for mobile robots, and more.

Wed 20 Oct

Displayed time zone: Central Time (US & Canada) change

07:40 - 09:00
Distributed Programming - mirrorOOPSLA at Zurich B
Chair(s): Shigeru Chiba The University of Tokyo
07:40
15m
Talk
A Multiparty Session Typing Discipline for Fault-Tolerant Event-Driven Distributed ProgrammingVirtual
OOPSLA
Malte Viering TU Darmstadt, Raymond Hu Queen Mary University of London, Patrick Eugster USI Lugano; Purdue University, Lukasz Ziarek University at Buffalo
DOI
07:55
15m
Talk
Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed SystemsIn-Person
OOPSLA
Wolf Honore Yale University, Jieung Kim Yale University, Ji-Yong Shin Northeastern University, Zhong Shao Yale University
DOI
08:10
15m
Talk
Automatic Migration from Synchronous to Asynchronous JavaScript APIsIn-Person
OOPSLA
Satyajit Gokhale Northeastern University, Alexi Turcotte Northeastern University, Frank Tip Northeastern University
DOI
08:25
15m
Talk
QuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based SystemsIn-Person
OOPSLA
Nouraldin Jaber Purdue University, Christopher Wagner Purdue University, Swen Jacobs CISPA, Milind Kulkarni Purdue University, Roopsha Samanta Purdue University
DOI
08:40
20m
Live Q&A
Discussion, Questions and Answers
OOPSLA

15:40 - 17:00
Distributed ProgrammingOOPSLA at Zurich B -8h
Chair(s): Mohsen Lesani University of California at Riverside
15:40
15m
Talk
A Multiparty Session Typing Discipline for Fault-Tolerant Event-Driven Distributed ProgrammingVirtual
OOPSLA
Malte Viering TU Darmstadt, Raymond Hu Queen Mary University of London, Patrick Eugster USI Lugano; Purdue University, Lukasz Ziarek University at Buffalo
DOI
15:55
15m
Talk
Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed SystemsIn-Person
OOPSLA
Wolf Honore Yale University, Jieung Kim Yale University, Ji-Yong Shin Northeastern University, Zhong Shao Yale University
DOI
16:10
15m
Talk
Automatic Migration from Synchronous to Asynchronous JavaScript APIsIn-Person
OOPSLA
Satyajit Gokhale Northeastern University, Alexi Turcotte Northeastern University, Frank Tip Northeastern University
DOI
16:25
15m
Talk
QuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based SystemsIn-Person
OOPSLA
Nouraldin Jaber Purdue University, Christopher Wagner Purdue University, Swen Jacobs CISPA, Milind Kulkarni Purdue University, Roopsha Samanta Purdue University
DOI
16:40
20m
Live Q&A
Discussion, Questions and Answers
OOPSLA