QuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based Systems

Jaber, Nouraldin and Wagner, Christopher and Jacobs, Swen and Kulkarni, Milind and Samanta, Roopsha
(2021) QuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based Systems.
In: OOPSLA 2021.
Conference: OOPSLA ACM Conference on Object Oriented Programming Systems Languages and Applications
(In Press)

[img] Text
oopsla21main-p364-p-5120270dad-53724-submitted.pdf

Download (724kB)

Abstract

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.

Actions

Actions (login required)

View Item View Item