(2021) QuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based Systems.
|
Text
oopsla21main-p364-p-5120270dad-53724-submitted.pdf Download (724kB) | Preview |
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.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Divisions: | Swen Jacobs (SJ) |
| Conference: | OOPSLA ACM Conference on Object Oriented Programming Systems Languages and Applications |
| Depositing User: | Swen Jacobs |
| Date Deposited: | 24 Sep 2021 08:44 |
| Last Modified: | 24 Sep 2021 08:44 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/3482 |
Actions
Actions (login required)
 |
View Item |