CISPA
Browse
cispa_all_3482.pdf (707.85 kB)

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

Download (707.85 kB)
conference contribution
posted on 2023-11-29, 18:17 authored by Nouraldin Jaber, Christopher Wagner, Swen JacobsSwen Jacobs, Milind Kulkarni, Roopsha Samanta
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.

History

Preferred Citation

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

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

ACM Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA)

Legacy Posted Date

2021-09-24

Open Access Type

  • Green

BibTeX

@inproceedings{cispa_all_3482, title = "QuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based Systems", author = "Jaber, Nouraldin and Wagner, Christopher and Jacobs, Swen and Kulkarni, Milind and Samanta, Roopsha", booktitle="{ACM Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA)}", year="2021", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC