978-3-031-30820-8.pdf (15.12 MB)

Synthesis of Distributed Agreement-Based Systems with Efficiently-Decidable Verification

Download (15.12 MB)
conference contribution
posted on 2024-03-25, 12:55 authored by Nouraldin Jaber, Christopher Wagner, Swen Jacobs, Milind Kulkarni, Roopsha Samanta
Distributed agreement-based (DAB) systems use common distributed agreement protocols such as leader election and consensus as building blocks for their target functionality. While automated verification for DAB systems is undecidable in general, recent work identifies a large class of DAB systems for which verification is efficiently-decidable. Unfortunately, the conditions characterizing such a class can be opaque and non-intuitive, and can pose a significant challenge to system designers trying to model their systems in this class. In this paper, we present a synthesis-driven tool, CINNABAR, to help system designers building DAB systems ensure that their intended designs belong to an efficiently-decidable class. In particular, starting from an initial sketch provided by the designer, CINNABAR generates sketch completions using a counterexample-guided procedure. The core technique relies on compactly encoding root-causes of counterexamples to varied properties such as efficient-decidability and safety. We demonstrate CINNABAR ’s effectiveness by successfully and efficiently synthesizing completions for a variety of interesting DAB systems including a distributed key-value store and a distributed consortium system.


Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Tools and Algorithms for Construction and Analysis of Systems (TACAS)



Page Range



Springer Nature

Open Access Type

  • Hybrid


@inproceedings{Jaber:Wagner:Jacobs:Kulkarni:Samanta:2023, title = "Synthesis of Distributed Agreement-Based Systems with Efficiently-Decidable Verification", author = "Jaber, Nouraldin" AND "Wagner, Christopher" AND "Jacobs, Swen" AND "Kulkarni, Milind" AND "Samanta, Roopsha", year = 2023, month = 4, pages = "289--308", publisher = "Springer Nature", issn = "1611-3349", doi = "10.1007/978-3-031-30820-8_19" }