References & Citations
Computer Science > Programming Languages
Title: QuickSilver: A Modeling and Parameterized Verification Framework for Systems with Distributed Agreement (Extended Version)
(Submitted on 9 Apr 2020 (v1), last revised 13 Sep 2021 (this version, v3))
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.
Submission history
From: Nouraldin Jaber [view email][v1] Thu, 9 Apr 2020 15:48:28 GMT (1666kb,D)
[v2] Thu, 8 Oct 2020 05:42:23 GMT (1626kb,D)
[v3] Mon, 13 Sep 2021 14:24:48 GMT (876kb)
Link back to: arXiv, form interface, contact.