pith. sign in

arxiv: 2606.24003 · v1 · pith:3MZDXMCRnew · submitted 2026-06-22 · 💻 cs.PL · cs.LO

DissProve: Automated Verification of Distributed Protocols with Affine Communication

Christian Fontenot , Gowtham Kaki , Bor-Yuh Evan Chang This is my paper

Pith reviewed 2026-06-26 05:33 UTC · model grok-4.3

classification 💻 cs.PL cs.LO
keywords automated verificationdistributed protocolsaffine communicationsafety propertiesactor systemsparametric systemsbackward reasoningmaterialization
0
0 comments X

The pith

Safety properties of affine distributed protocols with unbounded actors can be verified automatically by backward reasoning from error states using goal-directed materialization, causality, and summarization.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper aims to show that the combinatorial explosion of execution histories in asynchronous parametric distributed systems can be tamed for a subclass called affine protocols, which have unbounded history length but only bounded communication rounds. It does so by replacing the need for complex global invariants with a goal-directed backward search that materializes relevant states, tracks causality, and summarizes histories to prove unreachability of error states. A sympathetic reader would care because this removes a major barrier to checking real actor-based systems that scale to any number of participants. The approach is realized in a prototype tool called DissProve that demonstrates feasibility on such protocols. If the method works as described, automated safety checking becomes practical for this important family of systems without manual invariant construction.

Core claim

We present an automated verification technique based on proving unreachability backwards from error states in an actor system. One key insight is that the unboundedness from parametricity can be further classified into affine and non-affine protocols, where affine protocols have execution histories of unbounded length in a bounded number of communication rounds. We show how to use novel, goal-directed notions of materialization, causality, and summarization to verify safety properties of affine protocols with an unbounded number of actors in an automated manner.

What carries the argument

Goal-directed materialization, causality, and summarization operations that operate on affine protocols (bounded communication rounds despite unbounded history length) to perform backward unreachability proofs.

If this is right

  • Safety verification of parametric actor systems becomes possible without constructing global invariants that span the entire system.
  • Unbounded numbers of actors can be handled automatically when communication rounds remain bounded.
  • Backward reasoning from error states replaces forward enumeration of histories that grow combinatorially with asynchrony.
  • The classification into affine protocols separates cases that admit this automated treatment from those that do not.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same backward machinery might be extended to check liveness or fairness properties if suitable summarization rules for those can be defined.
  • Protocols that are not affine may still become verifiable if they can be decomposed into affine sub-protocols.
  • The approach could reduce the manual effort required when porting verification from small fixed-size systems to their parametric versions.

Load-bearing premise

The protocols under verification must be affine, meaning their execution histories have unbounded length but only bounded communication rounds, and the materialization and summarization steps must capture every relevant history without omitting a counterexample.

What would settle it

An affine protocol containing a reachable safety violation that the DissProve tool reports as unreachable because its summarization operation failed to cover the violating execution history.

Figures

Figures reproduced from arXiv: 2606.24003 by Bor-Yuh Evan Chang, Christian Fontenot, Gowtham Kaki.

Figure 1
Figure 1. Figure 1: A simplified “one-shot” leader election pro [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Actor materialization instantiates the node [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Actor-causality reduction focuses on materializing the necessary message-sends to witness the message [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Handling the message segment Node c d𝑎bn3 .eVote𝑘3 () summarizes the handling of a sequence of 𝑘3 instances of the message −d𝑎bn3 .eVote () for arbitrary sending actors. Because our protocols are affine, we further derive 1 + 𝑘3 + 1 + 𝑘5 ≤ #Node c. Applying the effect of the forMe = forMe + 1 assignment leads to the store-constraint (𝑎bn1 .forMe + 1 + 1 > #Node c/2) at the pre-assignment location 𝑎bn1 ↦→ N… view at source ↗
Figure 5
Figure 5. Figure 5: Semantic domains for the dCSNH machine state. [PITH_FULL_IMAGE:figures/full_fig_p010_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Symbolically abstracting a dCSNH state using separation, linear, and ordered logics. [PITH_FULL_IMAGE:figures/full_fig_p012_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Causal dependence graphs abstract the causal-reduced abstract semantics [PITH_FULL_IMAGE:figures/full_fig_p021_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Runtime analysis of time spent resolving SMT queries on contradiction [PITH_FULL_IMAGE:figures/full_fig_p023_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Abstract syntax of dCSNH, a core language for reasoning about actor systems. [PITH_FULL_IMAGE:figures/full_fig_p029_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Initial States: To be initial, a state must only have actors at the idle location, messages for the initial [PITH_FULL_IMAGE:figures/full_fig_p033_10.png] view at source ↗
read the original abstract

We consider the problem of automatically proving safety properties of distributed protocols. Distributed protocols have been particularly challenging for automated verification due to their asynchronous and parametric nature. Compared to synchronous systems, asynchronous communication leads to a combinatorial explosion of possible execution histories of message handlers. And because distributed protocols are typically defined parametrically on the number of actors, these definitions lead to an unbounded number of possible execution histories of unbounded length. Existing verification techniques for such distributed protocols typically require global invariants about the entire actor system, which are complex even for simple protocols. In this paper, we present an automated verification technique based on proving unreachability backwards from error states in an actor system. One key insight is that the unboundedness from parametricity can be further classified into \emph{affine} and non-affine protocols, where affine protocols have execution histories of unbounded length in a bounded number of communication rounds. We show how to use novel, goal-directed notions of materialization, causality, and summarization to verify safety properties of affine protocols with an unbounded number of actors in an automated manner. Using our prototype verification tool DissProve, we provide evidence for the feasibility of automated safety verification of asynchronous parametrized systems with affine communication.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper claims to solve automated safety verification for parametric asynchronous distributed protocols by classifying them into affine (unbounded-length histories in bounded communication rounds) and non-affine, then using novel goal-directed materialization, causality, and summarization operators to perform backwards unreachability proofs from error states; feasibility is shown via the DissProve prototype.

Significance. If the materialization/summarization operators are complete for the affine class, the work would be significant as it enables automated verification without requiring manually supplied global invariants, addressing a long-standing challenge in parametric distributed-systems verification.

major comments (2)
  1. [Abstract and definition of affine class / operators] The central soundness claim rests on the unproven assertion that the goal-directed materialization, causality, and summarization operators generate all safety-relevant histories for affine protocols (the axiom that 'affine protocols admit bounded-round unbounded-length histories that can be summarized without loss of safety-relevant behaviors'). No completeness argument, external citation, or independent validation is supplied for this reduction; if any histories are pruned, backwards proofs become unsound by missing counterexamples.
  2. [Prototype evaluation section] The paper provides no derivation details, error bounds, or concrete example proofs in the abstract or visible structure; without these it is impossible to assess whether the prototype actually discharges the parametric unboundedness or merely restricts to a subclass where the new operators happen to work.
minor comments (1)
  1. Notation for the new operators (materialization, summarization) should be introduced with explicit syntax and semantics before use in the main claims.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the detailed and constructive feedback. We address the two major comments below and will revise the manuscript accordingly to strengthen the presentation of soundness and evaluation details.

read point-by-point responses

  1. Referee: [Abstract and definition of affine class / operators] The central soundness claim rests on the unproven assertion that the goal-directed materialization, causality, and summarization operators generate all safety-relevant histories for affine protocols (the axiom that 'affine protocols admit bounded-round unbounded-length histories that can be summarized without loss of safety-relevant behaviors'). No completeness argument, external citation, or independent validation is supplied for this reduction; if any histories are pruned, backwards proofs become unsound by missing counterexamples.

    Authors: The paper defines the affine class (Section 3) as protocols whose executions have unbounded-length histories confined to a bounded number of communication rounds. The materialization, causality, and summarization operators are presented as goal-directed constructions that exploit this bounded-round structure to preserve safety-relevant behaviors. While the technical development argues that the operators are sound and complete for this class by construction, we agree that an explicit standalone completeness theorem is not isolated as such. We will add a dedicated theorem and proof in the revised version establishing that, for any affine protocol, the operators generate all safety-relevant histories without pruning counterexamples. revision: yes

  2. Referee: [Prototype evaluation section] The paper provides no derivation details, error bounds, or concrete example proofs in the abstract or visible structure; without these it is impossible to assess whether the prototype actually discharges the parametric unboundedness or merely restricts to a subclass where the new operators happen to work.

    Authors: The evaluation (Section 6) reports successful verification runs on multiple affine protocols using DissProve, confirming that the tool handles parametric unboundedness for the defined class. As the procedure is a decision procedure rather than an approximation, error bounds do not apply. We acknowledge that the current presentation would benefit from expanded derivation details. We will revise the evaluation section and add an appendix containing concrete step-by-step example proofs for the case studies, making explicit how the operators discharge the unboundedness for the full affine class rather than a restricted subclass. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation self-contained

full rationale

The paper defines the affine protocol class and introduces novel goal-directed materialization, causality, and summarization operators as part of its verification technique. These definitions and their application to backwards unreachability checking do not reduce to fitted inputs renamed as predictions, self-cited uniqueness theorems, or any other enumerated circular pattern. The central claim rests on the internal soundness of the new operators for the defined class rather than any self-referential reduction or external self-citation chain. This is a standard case of a self-contained new method with no load-bearing circular steps.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 2 invented entities

The central claim rests on the newly introduced distinction between affine and non-affine protocols plus the sufficiency of the three new operators; these are defined within the paper rather than taken from prior literature.

axioms (2)
  • domain assumption Actor systems can be modeled with asynchronous message passing and parametric actor counts.
    Standard modeling assumption for distributed protocols invoked to frame the verification problem.
  • ad hoc to paper Affine protocols admit bounded-round unbounded-length histories that can be summarized without loss of safety-relevant behaviors.
    The key classification and summarization assumption introduced to make backward verification tractable.
invented entities (2)
  • affine protocol class no independent evidence
    purpose: To delineate the subset of parametric protocols amenable to the new verification technique.
    Defined in the paper to separate tractable from intractable cases.
  • goal-directed materialization operator no independent evidence
    purpose: To generate concrete states from abstract ones during backward search.
    Novel operator introduced by the paper.

pith-pipeline@v0.9.1-grok · 5745 in / 1519 out tokens · 21018 ms · 2026-06-26T05:33:47.485308+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

51 extracted references · 18 canonical work pages

  1. [1]

    Parosh Aziz Abdulla, Yu-Fang Chen, Giorgio Delzanno, Frédéric Haziza, Chih-Duo Hong, and Ahmed Rezine. 2010. Con- strained monotonic abstraction: A CEGAR for parameterized verification. InInternational Conference on Concurrency Theory. Springer, 86–101

    2010

  2. [2]

    Gul Agha. 1986. An overview of actor languages.ACM Sigplan Notices21, 10 (1986), 58–67

    1986

  3. [3]

    Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2005. Symbolic Execution with Separation Logic. In Programming Languages and Systems, Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2-5, 2005, Proceedings (Lecture Notes in Computer Science, Vol. 3780), Kwangkeun Yi (Ed.). Springer, 52–68. https://doi.org/10. 1007/11575467_5

    2005

  4. [4]

    Sam Blackshear, Bor-Yuh Evan Chang, and Manu Sridharan. 2013. Thresher: precise refutations for heap reachability. InACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, W A, USA, June 16-19, 2013, Hans-Juergen Boehm and Cormac Flanagan (Eds.). ACM, 275–286. https://doi.org/10.1145/2491956.2462186

    work page doi:10.1145/2491956.2462186 2013

  5. [5]

    Sam Blackshear, Bor-Yuh Evan Chang, and Manu Sridharan. 2015. Selective control-flow abstraction via jumping. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SPLASH 2015, Pittsburgh, PA, USA, October 25-30, 2015, Jonathan Aldrich and Patrick Eugster ...

    work page doi:10.1145/2814270.2814293 2015

  6. [6]

    Sascha Böhme and Tobias Nipkow. 2010. Sledgehammer: judgement day. InProceedings of the 5th International Conference on Automated Reasoning(Edinburgh, UK)(IJCAR’10). Springer-Verlag, Berlin, Heidelberg, 107–121. https: //doi.org/10.1007/978-3-642-14203-1_9

    work page doi:10.1007/978-3-642-14203-1_9 2010

  7. [7]

    Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, and Fatiha Zaïdi. 2012. Cubicle: a parallel SMT-based model checker for parameterized systems: tool paper. InInternational Conference on Computer Aided Verification. Springer, 718–724

    2012

  8. [8]

    Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. InProceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. 238–252

    1977

  9. [9]

    Giorgio Delzanno. 2003. Constraint-based verification of parameterized cache coherence protocols.Formal Methods in System Design23, 3 (2003), 257–301

    2003

  10. [10]

    Ankush Desai, Vivek Gupta, Ethan Jackson, Shaz Qadeer, Sriram Rajamani, and Damien Zufferey. 2013. P: safe asynchronous event-driven programming.ACM SIGPLAN Notices48, 6 (2013), 321–332

    2013

  11. [11]

    Cormac Flanagan and Patrice Godefroid. 2005. Dynamic partial-order reduction for model checking software.ACM Sigplan Notices40, 1 (2005), 110–121

    2005

  12. [12]

    Álvaro García-Pérez, Alexey Gotsman, Yuri Meshman, and Ilya Sergey. 2018. Paxos consensus, deconstructed and abstracted. InEuropean Symposium on Programming. Springer, 912–939

    2018

  13. [13]

    Silvio Ghilardi and Silvio Ranise. 2010. Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis.Logical Methods in Computer Science6 (2010)

    2010

  14. [14]

    Jean-Yves Girard. 1987. Linear Logic.Theor. Comput. Sci.50 (1987), 1–102. https://doi.org/10.1016/0304-3975(87)90045-4

    work page doi:10.1016/0304-3975(87)90045-4 1987

  15. [15]

    Jim Gray and Leslie Lamport. 2006. Consensus on transaction commit.ACM Trans. Database Syst.31, 1 (March 2006), 133–160. https://doi.org/10.1145/1132863.1132867

    work page doi:10.1145/1132863.1132867 2006

  16. [16]

    Nightingale, Matthew Renzelmann, Alex Shamis, Anirudh Badam, and Miguel Castro

    Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, and Brian Zill. 2015. IronFleet: Proving Practical Distributed Systems Correct. InProceedings of the 25th Symposium on Operating Systems Principles(Monterey, California)(SOSP ’15). Association for Computing Machinery, New York, NY, USA, 1–17. htt...

    work page doi:10.1145/2815400.2815428 2015

  17. [17]

    Jonas Kastberg Hinrichsen, Jesper Bengtson, and Robbert Krebbers. 2019. Actris: Session-Type Based Reasoning in Separation Logic.Proc. ACM Program. Lang.4, POPL, Article 6 (dec 2019), 30 pages. https://doi.org/10.1145/3371074

    work page doi:10.1145/3371074 2019

  18. [18]

    Ishtiaq and Peter W

    Samin S. Ishtiaq and Peter W. O’Hearn. 2001. BI as an Assertion Language for Mutable Data Structures. InConference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, January 17-19, 2001, Chris Hankin and Dave Schmidt (Eds.). ACM, 14–26. https://doi.org/10.1145/360204.375719

    work page doi:10.1145/360204.375719 2001

  19. [19]

    Nouraldin Jaber, Christopher Wagner, Swen Jacobs, Milind Kulkarni, and Roopsha Samanta. 2021. Quicksilver: modeling and parameterized verification for distributed agreement-based systems.Proceedings of the ACM on Programming Languages5, OOPSLA (2021), 1–31

    2021

  20. [20]

    Gowtham Kaki, Kapil Earanky, KC Sivaramakrishnan, and Suresh Jagannathan. 2018. Safe replication through bounded concurrency verification.Proc. ACM Program. Lang.2, OOPSLA, Article 164 (Oct. 2018), 27 pages. https: //doi.org/10.1145/3276534

    work page doi:10.1145/3276534 2018

  21. [21]

    Zachary Kincaid, Jason Breck, Ashkan Forouhi Boroujeni, and Thomas Reps. 2017. Compositional recurrence analysis revisited. InProceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (Barcelona, Spain)(PLDI 2017). Association for Computing Machinery, New York, NY, USA, 248–262. https://doi.org/ 10.1145/3062341.30623...

    work page doi:10.1145/3062341.3062373 2017

  22. [22]

    Zachary Kincaid, John Cyphert, Jason Breck, and Thomas Reps. 2017. Non-linear reasoning for invariant synthesis. Proceedings of the ACM on Programming Languages2, POPL (2017), 1–33

    2017

  23. [23]

    Igor Konnov, Jure Kukovec, and Thanh-Hai Tran. 2019. TLA+ model checking made symbolic.Proceedings of the ACM on Programming Languages3, OOPSLA (2019), 1–30

    2019

  24. [24]

    Igor Konnov, Jure Kukovec, and Thanh-Hai Tran. 2019. TLA+ model checking made symbolic.Proc. ACM Program. Lang.3, OOPSLA, Article 123 (Oct. 2019), 30 pages. https://doi.org/10.1145/3360549

    work page doi:10.1145/3360549 2019

  25. [25]

    Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede Gregersen, and Lars Birkedal

  26. [26]

    Aneris: A mechanised logic for modular reasoning about distributed systems. InProgramming Languages and Systems: 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings 29. Springer International Publishing, 336–365

    2020

  27. [27]

    Leslie Lamport. 1974. A new solution of Dijkstra’s concurrent programming problem.Commun. ACM17, 8 (Aug. 1974), 453–455. https://doi.org/10.1145/361082.361093

    work page doi:10.1145/361082.361093 1974

  28. [28]

    Leslie Lamport. 2001. Paxos made simple.ACM SIGACT News (Distributed Computing Column) 32, 4 (Whole Number 121, December 2001)(2001), 51–58

    2001

  29. [29]

    Lukman, and Haryadi S

    Tanakorn Leesatapornwongsa, Mingzhe Hao, Pallavi Joshi, Jeffrey F. Lukman, and Haryadi S. Gunawi. 2014. SAMC: semantic-aware model checking for fast discovery of deep bugs in cloud systems. InProceedings of the 11th USENIX Conference on Operating Systems Design and Implementation(Broomfield, CO)(OSDI’14). USENIX Association, USA, 399–414

    2014

  30. [30]

    K Rustan M Leino. 2010. Dafny: An automatic program verifier for functional correctness. InInternational conference on logic for programming artificial intelligence and reasoning. Springer, 348–370

    2010

  31. [31]

    Lewchenko, Gowtham Kaki, and Bor-Yuh Evan Chang

    Nicholas V. Lewchenko, Gowtham Kaki, and Bor-Yuh Evan Chang. 2025. Bolt-On Strong Consistency: Specification, Implementation, and Verification.Proc. ACM Program. Lang.9, OOPSLA1, Article 137 (April 2025), 28 pages. https: //doi.org/10.1145/3720502

    work page doi:10.1145/3720502 2025

  32. [32]

    Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci, and Karem A Sakallah. 2019. I4: incremental inference of inductive invariants for verification of distributed protocols. InProceedings of the 27th ACM Symposium on Operating Systems Principles. 370–384

    2019

  33. [33]

    Antoni Mazurkiewicz. 1984. Traces, histories, graphs: Instances of a process monoid. InInternational Symposium on Mathematical Foundations of Computer Science. Springer, 115–133

    1984

  34. [34]

    Shawn Meier, Sergio Mover, Gowtham Kaki, and Bor-Yuh Evan Chang. 2023. Historia: Refuting Callback Reachability with Message-History Logics.Proceedings of the ACM on Programming Languages7, OOPSLA2 (2023), 1905–1934

    2023

  35. [35]

    Diego Ongaro and John Ousterhout. 2014. In search of an understandable consensus algorithm. InProceedings of the 2014 USENIX Conference on USENIX Annual Technical Conference(Philadelphia, PA)(USENIX ATC’14). USENIX Association, USA, 305–320

    2014

  36. [36]

    Oded Padon, Giuliano Losa, Mooly Sagiv, and Sharon Shoham. 2017. Paxos made EPR: decidable reasoning about distributed protocols.Proceedings of the ACM on Programming Languages1, OOPSLA (2017), 1–31

    2017

  37. [37]

    Oded Padon, Kenneth L McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. 2016. Ivy: safety verification by interactive generalization. InProceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. 614–630

    2016

  38. [38]

    Lauren Pick, Ankush Desai, and Aarti Gupta. 2023. Psym: Efficient Symbolic Exploration of Distributed Systems. Proceedings of the ACM on Programming Languages7, PLDI (2023), 660–685

    2023

  39. [39]

    Jeff Polakow and Frank Pfenning. 1999. Natural deduction for intuitionistic non-commutative linear logic. InInterna- tional Conference on Typed Lambda Calculi and Applications. Springer, 295–309

    1999

  40. [40]

    Reynolds

    John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings. IEEE Computer Society, 55–74. https://doi.org/10.1109/LICS.2002.1029817

    work page doi:10.1109/lics.2002.1029817 2002

  41. [41]

    Ilya Sergey, James R Wilcox, and Zachary Tatlock. 2017. Programming and proving with distributed protocols. Proceedings of the ACM on Programming Languages2, POPL (2017), 1–30

    2017

  42. [42]

    Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, Frans Kaashoek, and Nickolai Zeldovich. 2023. Grove: a separation- logic library for verifying distributed systems. InProceedings of the 29th Symposium on Operating Systems Principles. 113–129

    2023

  43. [43]

    Wolf, Peter Müller, Martin Clochard, and David Basin

    Christoph Sprenger, Tobias Klenze, Marco Eilers, Felix A. Wolf, Peter Müller, Martin Clochard, and David Basin. 2020. Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification.Proc. ACM Program. Lang.4, OOPSLA, Article 152 (nov 2020), 31 pages. https://doi.org/10.1145/3428220

    work page doi:10.1145/3428220 2020

  44. [44]

    McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R

    Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, and Doug Woos. 2018. Modularity for decidability of deductive verification with applications to distributed systems. SIGPLAN Not.53, 4 (June 2018), 662–677. https://doi.org/10.1145/3296979.3192414 28 Christian Fontenot, Gowtham Kaki, and Bor-Yuh Evan Chang

    work page doi:10.1145/3296979.3192414 2018

  45. [45]

    Gleissenthall, Rami Gökhan Kıcı, Alexander Bakst, Deian Stefan, and Ranjit Jhala

    Klaus v. Gleissenthall, Rami Gökhan Kıcı, Alexander Bakst, Deian Stefan, and Ranjit Jhala. 2019. Pretend synchrony: synchronous verification of asynchronous distributed programs.Proceedings of the ACM on Programming Languages3, POPL (2019), 1–30

    2019

  46. [46]

    David Van Horn and Matthew Might. 2010. Abstracting abstract machines. InProceedings of the 15th ACM SIGPLAN international conference on Functional programming. 51–62

    2010

  47. [47]

    Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D

    James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson

  48. [48]

    https://doi.org/10.1145/2813885.2737958

    Verdi: A Framework for Implementing and Formally Verifying Distributed Systems.SIGPLAN Not.50, 6 (jun 2015), 357–368. https://doi.org/10.1145/2813885.2737958

    work page doi:10.1145/2813885.2737958 2015

  49. [49]

    Wilcox, Steve Anton, Zachary Tatlock, Michael D

    Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas Anderson. 2016. Planning for change in a formal verification of the raft consensus protocol. InProceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs(St. Petersburg, FL, USA)(CPP 2016). Association for Computing Machinery, New York, NY, USA, 154–...

    work page doi:10.1145/2854065.2854081 2016

  50. [50]

    Jianan Yao, Runzhou Tao, Ronghui Gu, and Jason Nieh. 2022. DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols. In16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22). USENIX Association, Carlsbad, CA, 485–501. https://www.usenix.org/conference/osdi22/presentation/yao

    2022

  51. [51]

    Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, and Gabriel Ryan. 2021. DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21). USENIX Association, 405–421. https://www.usenix.org/conference/osdi21/presentation/yao DissProve: Automated Verifi...

    2021