pith. sign in

arxiv: 2404.18048 · v2 · submitted 2024-04-28 · 💻 cs.DC · cs.LO

Interactive Safety Verification of Distributed Protocols by Inductive Proof Decomposition

William Schultz , Edward Ashton , Heidi Howard , Stavros Tripakis This is my paper

Pith reviewed 2026-05-24 01:50 UTC · model grok-4.3

classification 💻 cs.DC cs.LO
keywords inductive proof decompositioninductive proof graphsafety verificationdistributed protocolsRaft consensusinductive invariantsvariable slicinginteractive verification
0
0 comments X

The pith

Inductive proof decomposition lets humans build safety invariants for distributed protocols by constructing proof graphs backwards from the target property.

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

The paper presents inductive proof decomposition as a methodology for interactive safety verification of distributed protocols. It structures development around an inductive proof graph that a verifier builds incrementally from the safety property, localizing induction counterexamples to individual nodes and decomposing nodes according to logical actions in the protocol transition relation. Localized variable slicing then hides irrelevant state at each sub-component. This approach produces complete inductive invariants for protocols such as Raft that lie beyond current automated verification tools. A reader would care because it supplies a concrete way to guide human effort on large verification tasks where automation alone is insufficient.

Core claim

Inductive proof decomposition organizes the development of an inductive invariant as an inductive proof graph built backwards from a target safety property; nodes of the graph are refined using induction counterexamples localized to those nodes and further decomposed according to the logical actions of the protocol's transition relation, with variable slicing applied locally at each node to reduce the visible state.

What carries the argument

The inductive proof graph, which structures inductive invariant development by localizing counterexamples to nodes and supporting decomposition based on protocol actions.

If this is right

  • Safety proofs become feasible for protocols such as Raft that exceed the reach of automated tools.
  • The resulting proof graphs expose the internal structure of a protocol's correctness argument.
  • Variable slicing at each node reduces the state a verifier must consider at any one step.
  • Localized counterexamples guide incremental refinement rather than requiring a single monolithic invariant.

Where Pith is reading between the lines

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

  • The same graph-based decomposition could be tested on verification tasks outside distributed systems, such as concurrent software with large state spaces.
  • Proof graphs might function as human-readable records of why a protocol satisfies its safety property.
  • Parts of node decomposition or slicing might be automated and combined with existing model checkers.

Load-bearing premise

Induction counterexamples can be localized to specific nodes of the proof graph and those nodes can be decomposed based on the protocol's transition actions in a manner that permits successful completion for complex protocols.

What would settle it

An attempt to construct a complete inductive proof graph for the Raft protocol that fails to resolve all induction counterexamples even after repeated localization, decomposition, and variable slicing.

Figures

Figures reproduced from arXiv: 2404.18048 by Edward Ashton, Heidi Howard, Stavros Tripakis, William Schultz.

Figure 1
Figure 1. Figure 1: State variables, initial states (Init), transition relation (Next), and safety property (NoConflictingValues) for the SimpleConsensus protocol. Definitions of the protocol actions are shown on the right. • Definition and formalization of inductive proof graphs, a formal structure representing the logical dependencies between conjuncts of an inductive invariant and actions of a distributed or concurrent pro… view at source ↗
Figure 2
Figure 2. Figure 2: Complete inductive invariant, Ind, for proving the NoConflictingValues safety property of the Simple￾Consensus protocol from [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Example progression of inductive proof graph for [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: A complete inductive proof graph for SimpleConsensus protocol inductive invariant and NoConflict￾ingValues safety property (the root node). Local variable slices are shown as , along with the size of the explored state set slice at that node, indicated as ||, along with the reduction factor over the full set of explored states computed during inference runs of SimpleConsensus. lemmas create new proof oblig… view at source ↗
Figure 5
Figure 5. Figure 5: Full grammar and some grammar slices for [PITH_FULL_IMAGE:figures/full_fig_p007_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Sample inductive proof graph. Lemma nodes are depict [PITH_FULL_IMAGE:figures/full_fig_p010_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Complete, synthesized inductive proof graph for the [PITH_FULL_IMAGE:figures/full_fig_p018_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Synthesized AsyncRa inductive proof graph for proof of the ElectionSafety property. largest benchmark we test, and we are able to synthesize an inductive proof graph for the Election￾Safety property in just under 4 hours. We sample a set of 10,000,000 reachable states for the set || for this benchmark, and, similarly, the performance is heavily impacted by the gains from state slicing during these inferenc… view at source ↗
Figure 9
Figure 9. Figure 9: Incomplete AsyncRa inductive proof graph for proof of the ElectionSafety property that was synthe￾sized when missing grammar predicates relating to vote request messages (voteReqs) and the locally recorded votes on servers (votedFor). represent, respectively, the actions a resource manager takes to commit or abort. That is, these are specifically the actions that can directly falsify the target safety prop… view at source ↗
read the original abstract

Many techniques for the automated verification of distributed protocols have been developed over the past several years, but their performance is still unpredictable and their failure modes can be opaque for industrial scale verification tasks. Thus, in practice, large-scale verification efforts typically require some amount of human guidance. In this paper, we present inductive proof decomposition, a new methodology for interactive safety verification that provides a compositional, interactive approach to inductive invariant development. Our approach guides the human-aided development of inductive invariants via a novel structure, an inductive proof graph, which is built incrementally by a human verifier, working backwards from a target safety property. A user is guided by induction counterexamples that are localized to specific nodes of this graph, and nodes of this proof graph are further decomposed based on logical actions that appear in a protocol's transition relation. Our decomposition also enables a localized variable slicing technique that hides irrelevant protocol state at each sub-component of an inductive proof, allowing a user to focus on fine-grained sub-problems rather than a large, monolithic inductive invariant. We present our technique and experience applying it to develop inductive safety proofs of several complex distributed protocols, including the Raft consensus protocol, which is beyond the capabilities of modern automated verification tools. We also demonstrate how the developed proof graphs provide additional insight into the structure of a protocol proof and its correctness.

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 / 2 minor

Summary. The paper introduces inductive proof decomposition as an interactive methodology for safety verification of distributed protocols. It constructs an inductive proof graph backwards from a target safety property, localizes induction counterexamples to specific graph nodes, decomposes nodes according to logical actions in the protocol transition relation, and applies localized variable slicing to hide irrelevant state. The approach is presented as guiding human-aided invariant development and is demonstrated via experience reports on several protocols, including Raft, which the authors state is beyond the capabilities of modern automated verification tools. The developed proof graphs are also claimed to provide insight into protocol structure.

Significance. If the central claims hold, the work offers a structured, compositional framework that could meaningfully assist human verifiers in tackling complex distributed protocols where fully automated tools fail. The inductive proof graph and slicing technique address the practical difficulty of monolithic invariants, and the reported application to Raft constitutes a non-trivial case study. The methodology is scoped to interactive use rather than full automation, which aligns with the acknowledged need for human guidance in large-scale verification.

major comments (2)
  1. [§5] §5 (Raft case study): the claim that the method succeeds on Raft where automated tools fail lacks specific details on graph construction, node decompositions performed, counterexample localizations, or slicing applications; this evidence is load-bearing for assessing whether the localization and decomposition assumptions enable verification as stated.
  2. [§3.2] §3.2 (decomposition rules): the argument that induction counterexamples can be localized to nodes and that nodes can be decomposed by logical actions without compromising overall soundness requires an explicit invariant or lemma showing preservation of the inductive property across the graph; without it the central methodology's correctness is not fully established.
minor comments (2)
  1. The abstract would be strengthened by including one concrete example of a decomposed sub-problem or the scale of the Raft proof graph.
  2. [§3] Notation for the inductive proof graph (nodes, edges, and slicing) should be introduced with a small running example before the general definitions.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the detailed and constructive review. We address the two major comments below and will incorporate revisions to strengthen the presentation of both the Raft case study and the soundness argument.

read point-by-point responses

  1. Referee: [§5] §5 (Raft case study): the claim that the method succeeds on Raft where automated tools fail lacks specific details on graph construction, node decompositions performed, counterexample localizations, or slicing applications; this evidence is load-bearing for assessing whether the localization and decomposition assumptions enable verification as stated.

    Authors: We agree that §5 would benefit from additional concrete details to make the Raft experience report more self-contained. The current text describes the overall structure of the proof graph and notes that automated tools could not complete the verification, but does not enumerate every decomposition step or slicing application. In the revised manuscript we will add a table or expanded narrative listing the principal nodes, the logical actions used for each decomposition, representative localized counterexamples, and the variables sliced at each node. This will allow readers to evaluate how the methodology scales to Raft without requiring them to reconstruct the full graph from the high-level description. revision: partial

  2. Referee: [§3.2] §3.2 (decomposition rules): the argument that induction counterexamples can be localized to nodes and that nodes can be decomposed by logical actions without compromising overall soundness requires an explicit invariant or lemma showing preservation of the inductive property across the graph; without it the central methodology's correctness is not fully established.

    Authors: The manuscript argues soundness by construction: the proof graph is built so that the conjunction of the per-node invariants implies the target safety property, and each decomposition step partitions the transition relation according to the protocol's logical actions while preserving the inductive step. However, we acknowledge that an explicit lemma stating the preservation property across the entire graph would make the argument easier to verify. We will add such a lemma (with a short proof sketch) to §3.2 in the revised version. revision: yes

Circularity Check

0 steps flagged

No significant circularity; new methodology is self-contained

full rationale

The paper presents a novel interactive methodology (inductive proof decomposition via proof graphs, counterexample localization, action-based node decomposition, and localized variable slicing) for human-guided invariant development. No equations, predictions, fitted parameters, or first-principles derivations appear in the provided text or abstract. Claims rest on the description of the technique and its reported application to protocols including Raft, without reduction to self-citations, self-definitions, or renamed known results. The approach is scoped as a human-aided process independent of prior fitted results, making the derivation chain self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Based on the abstract, no free parameters, axioms, or invented entities are explicitly described; the method relies on standard concepts in formal verification but details are not provided.

pith-pipeline@v0.9.0 · 5766 in / 1192 out tokens · 30107 ms · 2026-05-24T01:50:59.380226+00:00 · methodology

discussion (0)

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

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy

    cs.LO 2026-04 unverdicted novelty 7.0

    An incremental safety proof system using forward-backward reasoning and prophecy steps allows proving safety with simpler invariants than a single complex inductive invariant.

Reference graph

Works this paper leans on

49 extracted references · 49 canonical work pages · cited by 1 Pith paper

  1. [1]

    A., M/a.sc/n.sc/g.sc, F

    A/l.sc/u.sc/r.sc, R., H/e.sc/n.sc/z.sc/i.sc/n.sc/g.sc/e.sc/r.sc, T. A., M/a.sc/n.sc/g.sc, F. Y. C., Q/a.sc/d.sc/e.sc/e.sc/r.sc, S., R/a.sc/j.sc/a.sc/m.sc/a.sc/n.sc/i.sc, S. K., /a.sc/n.sc/d.sc T/a.sc/s.sc/i.sc/r.sc/a.sc/n.sc, S.Mocha: Modularity in model checking. In Computer Aided Verification (Berlin, Heidelberg, 1998), A. J. Hu and M. Y. Vardi, Eds., Sp...

    work page 1998

  2. [2]

    In 2017 Formal Methods in Computer Aided Design (FMCAD) (2017), IEEE, pp

    B/e.sc/r.sc/r.sc/y.sc/h.sc/i.sc/l.sc/l.sc, R., I/v.sc/r.sc/i.sc/i.sc, A., V/e.sc/i.sc/r.sc/a.sc, N., /a.sc/n.sc/d.sc V/e.sc/n.sc/e.sc/r.sc/i.sc/s.sc, A.Learning support sets in IC3 and Quip: The good, the bad, and the ugly. In 2017 Formal Methods in Computer Aided Design (FMCAD) (2017), IEEE, pp. 140–147

    work page 2017

  3. [3]

    M., S/t.sc/r.sc/i.sc/c.sc/h.sc/m.sc/a.sc/n.sc, O., /a.sc/n.sc/d.sc Z/h.sc/u.sc, Y

    B/i.sc/e.sc/r.sc/e.sc, A., C/i.sc/m.sc/a.sc/t.sc/t.sc/i.sc, A., C/l.sc/a.sc/r.sc/k.sc/e.sc, E. M., S/t.sc/r.sc/i.sc/c.sc/h.sc/m.sc/a.sc/n.sc, O., /a.sc/n.sc/d.sc Z/h.sc/u.sc, Y. Bounded model checking. Adv. Comput. 58 (2003), 117–148

    work page 2003

  4. [4]

    In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020) (2020), Schloss Dagstuhl-Leibniz-Zentrum für Informatik

    B/r.sc/a.sc/i.sc/t.sc/h.sc/w.sc/a.sc/i.sc/t.sc/e.sc, S., B/u.sc/c.sc/h.sc/m.sc/a.sc/n.sc, E., K/o.sc/n.sc/n.sc/o.sc/v.sc, I., M/i.sc/l.sc/o.sc/s.sc/e.sc/v.sc/i.sc/c.sc, Z., S/t.sc/o.sc/i.sc/l.sc/k.sc/o.sc/v.sc/s.sc/k.sc/a.sc, I., W/i.sc/d.sc/d.sc/e.sc/r.sc, J., /a.sc/n.sc/d.sc Z/a.sc/m.sc/f.sc/i.sc/r.sc, A.Formal Specification and Model Checking of the Ten...

    work page 2020

  5. [5]

    M., G/i.sc/a.sc/n.sc/n.sc/a.sc/k.sc/o.sc/p.sc/o.sc/u.sc/l.sc/o.sc/u.sc, D., /a.sc/n.sc/d.sc P/abreve.sc/s.sc/abreve.sc/r.sc/e.sc/a.sc/n.sc/u.sc, C

    C/o.sc/b.sc/l.sc/e.sc/i.sc/g.sc/h.sc, J. M., G/i.sc/a.sc/n.sc/n.sc/a.sc/k.sc/o.sc/p.sc/o.sc/u.sc/l.sc/o.sc/u.sc, D., /a.sc/n.sc/d.sc P/abreve.sc/s.sc/abreve.sc/r.sc/e.sc/a.sc/n.sc/u.sc, C. S.Learning assumptions for compositional verification. In Tools and Algorithms for the Construction and Analysis of Sy stems: 9th International Conference, TACAS 2003 He...

    work page 2003

  6. [6]

    C/o.sc/r.sc/b.sc/e.sc/t.sc/t.sc, J. C., D/e.sc/a.sc/n.sc, J., E/p.sc/s.sc/t.sc/e.sc/i.sc/n.sc, M., F/i.sc/k.sc/e.sc/s.sc, A., F/r.sc/o.sc/s.sc/t.sc, C., F/u.sc/r.sc/m.sc/a.sc/n.sc, J., G/h.sc/e.sc/m.sc/a.sc/w.sc/a.sc/t.sc, S., G/u.sc/b.sc/a.sc/r.sc/e.sc/v.sc, A., H/e.sc/i.sc/s.sc/e.sc/r.sc, C., H/o.sc/c.sc/h.sc/s.sc/c.sc/h.sc/i.sc/l.sc/d.sc, P., H/s.sc/i....

    work page 2012

  7. [7]

    Proceedings of the 18th International Symposium on Formal Methods (FM 2012 ), Dimitra Giannakopoulou and Dominique Mery, editors

    C/o.sc/u.sc/s.sc/i.sc/n.sc/e.sc/a.sc/u.sc, D., D/o.sc/l.sc/i.sc/g.sc/e.sc/z.sc, D., L/a.sc/m.sc/p.sc/o.sc/r.sc/t.sc, L., M/e.sc/r.sc/z.sc, S., R/i.sc/c.sc/k.sc/e.sc/t.sc/t.sc/s.sc, D., /a.sc/n.sc/d.sc V /a.sc/n.sc/z.sc/e.sc/t.sc/t.sc/o.sc, H.TLA+ Proofs. Proceedings of the 18th International Symposium on Formal Methods (FM 2012 ), Dimitra Giannakopoulou a...

    work page 2012

  8. [8]

    D., P/e.sc/r.sc/k.sc/i.sc/n.sc/s.sc, J

    E/r.sc/n.sc/s.sc/t.sc, M. D., P/e.sc/r.sc/k.sc/i.sc/n.sc/s.sc, J. H., G/u.sc/o.sc, P. J., M/c.scC/a.sc/m.sc/a.sc/n.sc/t.sc, S., P/a.sc/c.sc/h.sc/e.sc/c.sc/o.sc, C., T/s.sc/c.sc/h.sc/a.sc/n.sc/t.sc/z.sc, M. S., /a.sc/n.sc/d.sc X/i.sc/a.sc/o.sc, C.The Daikon system for dynamic detection of likely invariants. Science of computer programming 69 , 1-3 (2007), 35–45

    work page 2007

  9. [9]

    In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13, Rome, Italy - January 23 - 25, 2013 (2013), R

    F/a.sc/r.sc/z.sc/a.sc/n.sc, A., K/i.sc/n.sc/c.sc/a.sc/i.sc/d.sc, Z., /a.sc/n.sc/d.sc P/o.sc/d.sc/e.sc/l.sc/s.sc/k.sc/i.sc, A.Inductive Data Flow Graphs. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13, Rome, Italy - January 23 - 25, 2013 (2013), R. Giacobazzi and R. Cousot, Eds., ACM, pp. 129–142

    work page 2013

  10. [10]

    In Tools and Algorithms for the Construction and Analysis of Systems (Cham, 2018), D

    F/e.sc/d.sc/y.sc/u.sc/k.sc/o.sc/v.sc/i.sc/c.sc/h.sc, G., /a.sc/n.sc/d.sc B/o.sc/d.sc/iacute.sc/k.sc, R.Accelerating Syntax-Guided Invariant Synthesis. In Tools and Algorithms for the Construction and Analysis of Systems (Cham, 2018), D. Beyer and M. Huisman, Eds., Springer International Pu blishing, pp. 251–269

    work page 2018

  11. [11]

    F/l.sc/a.sc/n.sc/a.sc/g.sc/a.sc/n.sc, C., /a.sc/n.sc/d.sc L/e.sc/i.sc/n.sc/o.sc, K. R. M.Houdini, an Annotation Assistant for ESC/Java. In Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity (Berlin, Heidelberg, 2001), FME ’01, Springer-Verlag, p. 500–517

    work page 2001

  12. [12]

    In NASA Formal Methods: 13th International Symposium, NFM 202 1, Virtual Event, May 24–28, 2021, Proceedings (Berlin, Heidelberg, 2021), Springer-Verlag, p

    G/o.sc/e.sc/l.sc, A., /a.sc/n.sc/d.sc S/a.sc/k.sc/a.sc/l.sc/l.sc/a.sc/h.sc, K.On Symmetry and Quantification: A New Approach to Verify Distributed P rotocols. In NASA Formal Methods: 13th International Symposium, NFM 202 1, Virtual Event, May 24–28, 2021, Proceedings (Berlin, Heidelberg, 2021), Springer-Verlag, p. 131–150

    work page 2021

  13. [13]

    A.Towards an Automatic Proof of Lamport’s Paxos

    G/o.sc/e.sc/l.sc, A., /a.sc/n.sc/d.sc S/a.sc/k.sc/a.sc/l.sc/l.sc/a.sc/h.sc, K. A.Towards an Automatic Proof of Lamport’s Paxos. 2021 Formal Methods in Computer Aided Design (FMCAD) (2021), 112–122

    work page 2021

  14. [14]

    J., K/a.sc/u.sc/f.sc/m.sc/a.sc/n.sc/n.sc, M., /a.sc/n.sc/d.sc R/a.sc/y.sc, S.The Right Tools for the Job: Correctness of Cone of Influence Reduct ion Proved Using ACL2 and HOL4

    G/o.sc/r.sc/d.sc/o.sc/n.sc, M. J., K/a.sc/u.sc/f.sc/m.sc/a.sc/n.sc/n.sc, M., /a.sc/n.sc/d.sc R/a.sc/y.sc, S.The Right Tools for the Job: Correctness of Cone of Influence Reduct ion Proved Using ACL2 and HOL4. J. Autom. Reason. 47 , 1 (jun 2011), 1–16

    work page 2011

  15. [15]

    In Operating Systems, An Advanced Course (Berlin, Heidelberg, 1978), Springer-Verlag, p

    G/r.sc/a.sc/y.sc, J.Notes on data base operating systems. In Operating Systems, An Advanced Course (Berlin, Heidelberg, 1978), Springer-Verlag, p. 393–481

    work page 1978

  16. [16]

    2015 Formal Methods in Computer-Aided Design (FMCAD) (2015), 65–72

    G/u.sc/r.sc/f.sc/i.sc/n.sc/k.sc/e.sc/l.sc, A., /a.sc/n.sc/d.sc I/v.sc/r.sc/i.sc/i.sc, A.Pushing to the top. 2015 Formal Methods in Computer-Aided Design (FMCAD) (2015), 65–72

    work page 2015

  17. [17]

    In 18th USENIX Symposium on Networked Systems Design and Imple mentation (NSDI 21) (Apr

    H/a.sc/n.sc/c.sc/e.sc, T., H/e.sc/u.sc/l.sc/e.sc, M., M/a.sc/r.sc/t.sc/i.sc/n.sc/s.sc, R., /a.sc/n.sc/d.sc P/a.sc/r.sc/n.sc/o.sc, B.Finding Invariants of Distributed Systems: It’s a Small (Enough) World After All. In 18th USENIX Symposium on Networked Systems Design and Imple mentation (NSDI 21) (Apr. 2021), USENIX Association, pp. 115–131

    work page 2021

  18. [18]

    J.The model checker SPIN

    H/o.sc/l.sc/z.sc/m.sc/a.sc/n.sc/n.sc, G. J.The model checker SPIN. IEEE Transactions on software engineering 23 , 5 (1997), 279–295

    work page 1997

  19. [19]

    H/u.sc/a.sc/n.sc/g.sc, D., L/i.sc/u.sc, Q., C/u.sc/i.sc, Q., F/a.sc/n.sc/g.sc, Z., M/a.sc, X., X/u.sc, F., S/h.sc/e.sc/n.sc, L.,T/a.sc/n.sc/g.sc, L., Z/h.sc/o.sc/u.sc, Y., H/u.sc/a.sc/n.sc/g.sc, M., W/e.sc/i.sc, W., L/i.sc/u.sc, C., Z/h.sc/a.sc/n.sc/g.sc, J., L/i.sc, J., W/u.sc, X., S/o.sc/n.sc/g.sc, L., S/u.sc/n.sc, R., Y/u.sc, S., Z/h.sc/a.sc/o.sc, L., ...

    work page 2020

  20. [20]

    A., /a.sc/n.sc/d.sc S/a.sc/n.sc/t.sc/o.sc/s.sc/a.sc, A

    J/a.sc/f.sc/f.sc/a.sc/r.sc, J., M/u.sc/r.sc/a.sc/l.sc/i.sc, V., N/a.sc/v.sc/a.sc/s.sc, J. A., /a.sc/n.sc/d.sc S/a.sc/n.sc/t.sc/o.sc/s.sc/a.sc, A. E.Path-sensitive backward slicing. In Static Analysis: 19th International Symposium, SAS 2012, Deauville, France, Sep tember 11-13, 2012. Proceedings 19 (2012), Springer, pp. 231– 247

    work page 2012

  21. [21]

    In Proceedings of the 2005 ACM SIGPLAN Conference on Programmi ng language Design and Implementation (2005), pp

    J/h.sc/a.sc/l.sc/a.sc, R., /a.sc/n.sc/d.sc M/a.sc/j.sc/u.sc/m.sc/d.sc/a.sc/r.sc, R.Path slicing. In Proceedings of the 2005 ACM SIGPLAN Conference on Programmi ng language Design and Implementation (2005), pp. 38–47

    work page 2005

  22. [22]

    K/a.sc/r.sc/b.sc/y.sc/s.sc/h.sc/e.sc/v.sc, A., B/j.sc/oslash.sc/r.sc/n.sc/e.sc/r.sc, N., I/t.sc/z.sc/h.sc/a.sc/k.sc/y.sc, S., R/i.sc/n.sc/e.sc/t.sc/z.sc/k.sc/y.sc, N., /a.sc/n.sc/d.sc S/h.sc/o.sc/h.sc/a.sc/m.sc, S.Property-Directed Inference of Universal Invariants or Proving Their Absence. J. ACM 64, 1 (mar 2017)

    work page 2017

  23. [23]

    K/a.sc/t.sc/s.sc/a.sc/r.sc/a.sc/k.sc/i.sc/s.sc, A., G/a.sc/v.sc/r.sc/i.sc/e.sc/l.sc/a.sc/t.sc/o.sc/s.sc, V., K/a.sc/t.sc/e.sc/b.sc/z.sc/a.sc/d.sc/e.sc/h.sc, M. S., J/o.sc/s.sc/h.sc/i.sc,A., D/r.sc/a.sc/g.sc/o.sc/j.sc/e.sc/v.sc/i.sc/c.sc, A., G/r.sc/o.sc/t.sc, B., /a.sc/n.sc/d.sc N/a.sc/g.sc/a.sc/r.sc/a.sc/j.sc/a.sc/n.sc, V.Her- mes: A fast, fault-tolerant...

    work page 2020

  24. [24]

    Zeus: Locality-aware distributed transactions

    K/a.sc/t.sc/s.sc/a.sc/r.sc/a.sc/k.sc/i.sc/s.sc, A., M/a.sc, Y., T/a.sc/n.sc, Z., B/a.sc/i.sc/n.sc/b.sc/r.sc/i.sc/d.sc/g.sc/e.sc, A., B/a.sc/l.sc/k.sc/w.sc/i.sc/l.sc/l.sc, M., D/r.sc/a.sc/g.sc/o.sc/j.sc/e.sc/v.sc/i.sc/c.sc, A., G/r.sc/o.sc/t.sc, B., R/a.sc/d.sc/u.sc/n.sc/o.sc/v.sc/i.sc/c.sc, B., /a.sc/n.sc/d.sc Z/h.sc/a.sc/n.sc/g.sc, Y. Zeus: Locality-awar...

    work page 2021

  25. [25]

    R., P/a.sc/d.sc/o.sc/n.sc, O., I/m.sc/m.sc/e.sc/r.sc/m.sc/a.sc/n.sc, N., /a.sc/n.sc/d.sc A/i.sc/k.sc/e.sc/n.sc, A.First-Order Quantified Separators

    K/o.sc/e.sc/n.sc/i.sc/g.sc, J. R., P/a.sc/d.sc/o.sc/n.sc, O., I/m.sc/m.sc/e.sc/r.sc/m.sc/a.sc/n.sc, N., /a.sc/n.sc/d.sc A/i.sc/k.sc/e.sc/n.sc, A.First-Order Quantified Separators. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and I mplementation (2020), PLDI 2020, Association for Computing Machinery, p. 703–717

    work page 2020

  26. [26]

    K/o.sc/e.sc/n.sc/i.sc/g.sc, J. R., P/a.sc/d.sc/o.sc/n.sc, O., S/h.sc/o.sc/h.sc/a.sc/m.sc, S., /a.sc/n.sc/d.sc A/i.sc/k.sc/e.sc/n.sc, A.Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion. In Tools and Algorithms for the Construction and Analysis of Systems (Cham, 2022), D. Fisman and G. Rosu, Eds., Springer International Pu...

    work page 2022

  27. [27]

    L/a.sc/m.sc/p.sc/o.sc/r.sc/t.sc, L.A New Solution of Dijkstra’s Concurrent Programming Problem. Commun. ACM 17 , 8 (aug 1974), 453–455

    work page 1974

  28. [28]

    ACM SIGACT News (Distributed Computing Column) 32, 4 (Whole Number 121, December 2001) (2001), 51–58

    L/a.sc/m.sc/p.sc/o.sc/r.sc/t.sc, L.Paxos made simple. ACM SIGACT News (Distributed Computing Column) 32, 4 (Whole Number 121, December 2001) (2001), 51–58

    work page 2001

  29. [29]

    Addison-Wesley, Jun 2002

    L/a.sc/m.sc/p.sc/o.sc/r.sc/t.sc, L.Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Jun 2002

    work page 2002

  30. [30]

    http://lamport.azurewebsites.net/tla/inductive-invariant.pdf , 2018

    L/a.sc/m.sc/p.sc/o.sc/r.sc/t.sc, L.Using TLC to Check Inductive Invariance. http://lamport.azurewebsites.net/tla/inductive-invariant.pdf , 2018. , Vol. 1, No. 1, Article . Publication date: April 2024. 24 William Schultz, Edward Ashton, Heidi Howard, and Stavro s Tripakis

    work page 2018

  31. [31]

    In USENIX Annual Technical Conference (2022)

    M/a.sc, H., A/h.sc/m.sc/a.sc/d.sc, H., G/o.sc/e.sc/l.sc, A., G/o.sc/l.sc/d.sc/w.sc/e.sc/b.sc/e.sc/r.sc, E., J/e.sc/a.sc/n.sc/n.sc/i.sc/n.sc, J./hyphen.scB., K/a.sc/p.sc/r.sc/i.sc/t.sc/s.sc/o.sc/s.sc, M., /a.sc/n.sc/d.sc K/a.sc/s.sc/i.sc/k.sc/c.sc/i.sc, B.Sift: Using Refinement- guided Automation to Verify Complex Distributed Systems. In USENIX Annual Techn...

    work page 2022

  32. [32]

    Springer-Verlag, Berlin, Heidelberg, 1995

    M/a.sc/n.sc/n.sc/a.sc, Z., /a.sc/n.sc/d.sc P/n.sc/u.sc/e.sc/l.sc/i.sc, A.Temporal Verification of Reactive Systems: Safety . Springer-Verlag, Berlin, Heidelberg, 1995

    work page 1995

  33. [33]

    Science of Computer Programming 37, 1 (2000), 279–309

    M/c.scM/i.sc/l.sc/l.sc/a.sc/n.sc, K.A methodology for hardware verification using compositional model c hecking. Science of Computer Programming 37, 1 (2000), 279–309

    work page 2000

  34. [34]

    Doctoral thesis (2014)

    O/n.sc/g.sc/a.sc/r.sc/o.sc, D.Consensus: Bridging Theory and Practice. Doctoral thesis (2014)

    work page 2014

  35. [35]

    In Proceedings of the 2014 USENIX Conference on USENIX Annual Technical Conferen ce (USA, 2014), USENIX ATC’14, USENIX Association, pp

    O/n.sc/g.sc/a.sc/r.sc/o.sc, D., /a.sc/n.sc/d.sc O/u.sc/s.sc/t.sc/e.sc/r.sc/h.sc/o.sc/u.sc/t.sc, J.In Search of an Understandable Consensus Algorithm. In Proceedings of the 2014 USENIX Conference on USENIX Annual Technical Conferen ce (USA, 2014), USENIX ATC’14, USENIX Association, pp. 305–320

    work page 2014

  36. [36]

    In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposiu m on Principles of Programming Languages (New York, NY, USA, 2016), POPL ’16, Association for Computing Machiner y, p

    P/a.sc/d.sc/o.sc/n.sc, O., I/m.sc/m.sc/e.sc/r.sc/m.sc/a.sc/n.sc, N., S/h.sc/o.sc/h.sc/a.sc/m.sc, S., K/a.sc/r.sc/b.sc/y.sc/s.sc/h.sc/e.sc/v.sc, A., /a.sc/n.sc/d.sc S/a.sc/g.sc/i.sc/v.sc, M.Decidability of Inferring Inductive Invariants. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposiu m on Principles of Programming Languages (New York, NY, US...

    work page 2016

  37. [37]

    L., P/a.sc/n.sc/d.sc/a.sc, A., S/a.sc/g.sc/i.sc/v.sc, M., /a.sc/n.sc/d.sc S/h.sc/o.sc/h.sc/a.sc/m.sc,S

    P/a.sc/d.sc/o.sc/n.sc, O., M/c.scM/i.sc/l.sc/l.sc/a.sc/n.sc, K. L., P/a.sc/n.sc/d.sc/a.sc, A., S/a.sc/g.sc/i.sc/v.sc, M., /a.sc/n.sc/d.sc S/h.sc/o.sc/h.sc/a.sc/m.sc,S. Ivy: Safety Verification by Interactive General- ization. In Proceedings of the 37th ACM SIGPLAN Conference on Programmi ng Language Design and Implementation (New York, NY, USA, 2016), PLDI...

    work page 2016

  38. [38]

    In Proceedings of the 11th ACM SIGPLAN International Conferen ce on Certified Programs and Proofs (Philadelphia, PA, USA, 2022), CPP 2022, Association for Computing Machinery, p

    S/c.sc/h.sc/u.sc/l.sc/t.sc/z.sc, W., D/a.sc/r.sc/d.sc/i.sc/k.sc, I., /a.sc/n.sc/d.sc T/r.sc/i.sc/p.sc/a.sc/k.sc/i.sc/s.sc, S.Formal Verification of a Distributed Dynamic Reconfiguration Protoco l. In Proceedings of the 11th ACM SIGPLAN International Conferen ce on Certified Programs and Proofs (Philadelphia, PA, USA, 2022), CPP 2022, Association for Computin...

    work page 2022

  39. [39]

    In 2022 Formal Methods in Computer-Aided Design (FMCAD) (2022), IEEE, pp

    S/c.sc/h.sc/u.sc/l.sc/t.sc/z.sc, W., D/a.sc/r.sc/d.sc/i.sc/k.sc, I., /a.sc/n.sc/d.sc T/r.sc/i.sc/p.sc/a.sc/k.sc/i.sc/s.sc, S.Plain and Simple Inductive Invariant Inference for Distributed Protocol s in TLA+. In 2022 Formal Methods in Computer-Aided Design (FMCAD) (2022), IEEE, pp. 273–283

    work page 2022

  40. [40]

    In Computer Aided Verification - 26th International Conference, CA V 201 4, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014

    S/h.sc/a.sc/r.sc/m.sc/a.sc, R., /a.sc/n.sc/d.sc A/i.sc/k.sc/e.sc/n.sc, A.From Invariant Checking to Invariant Inference Using Randomized Search. In Computer Aided Verification - 26th International Conference, CA V 201 4, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings (2014), A. Biere and R. Bloem, Eds.,...

    work page 2014

  41. [41]

    In Proceedings of the 2020 ACM SIGMOD International Conferenc e on Management of Data (2020), SIGMOD ’20, Association for Computing Machinery, p

    T/a.sc/f.sc/t.sc, R., S/h.sc/a.sc/r.sc/i.sc/f.sc, I., M/a.sc/t.sc/e.sc/i.sc, A., V /a.sc/n.scB/e.sc/n.sc/s.sc/c.sc/h.sc/o.sc/t.sc/e.sc/n.sc, N., L/e.sc/w.sc/i.sc/s.sc, J., G/r.sc/i.sc/e.sc/g.sc/e.sc/r.sc, T., N/i.sc/e.sc/m.sc/i.sc, K., W/o.sc/o.sc/d.sc/s.sc, A., B/i.sc/r.sc/z.sc/i.sc/n.sc, A., P/o.sc/s.sc/s.sc, R., B/a.sc/r.sc/d.sc/e.sc/a.sc, P., R/a.sc/n...

    work page 2020

  42. [42]

    L., P/a.sc/d.sc/o.sc/n.sc, O., S/a.sc/g.sc/i.sc/v.sc, M., S/h.sc/o.sc/h.sc/a.sc/m.sc, S., W/i.sc/l.sc/c.sc/o.sc/x.sc, J

    T/a.sc/u.sc/b.sc/e.sc, M., L/o.sc/s.sc/a.sc, G., M/c.scM/i.sc/l.sc/l.sc/a.sc/n.sc, K. L., P/a.sc/d.sc/o.sc/n.sc, O., S/a.sc/g.sc/i.sc/v.sc, M., S/h.sc/o.sc/h.sc/a.sc/m.sc, S., W/i.sc/l.sc/c.sc/o.sc/x.sc, J. R., /a.sc/n.sc/d.sc W/o.sc/o.sc/s.sc, D.Modularity for decidability of deductive verification with applications to distribu ted systems. In Proceedings...

    work page 2018

  43. [43]

    T/i.sc/p.sc, F.A survey of program slicing techniques. J. Program. Lang. 3 (1994)

    work page 1994

  44. [44]

    https://github.com/Vanlightly/raft-tlaplus/blob/main/specifications/standard-raft/Raft.tla , 2023

    V /a.sc/n.sc/l.sc/i.sc/g.sc/h.sc/t.sc/l.sc/y.sc, J.raft-tlaplus: A TLA+ specification of the Raft distributed consens us algorithm. https://github.com/Vanlightly/raft-tlaplus/blob/main/specifications/standard-raft/Raft.tla , 2023. GitHub reposi- tory

    work page 2023

  45. [45]

    R., W/o.sc/o.sc/s.sc, D., P/a.sc/n.sc/c.sc/h.sc/e.sc/k.sc/h.sc/a.sc, P., T/a.sc/t.sc/l.sc/o.sc/c.sc/k.sc, Z., W /a.sc/n.sc/g.sc, X., E/r.sc/n.sc/s.sc/t.sc, M

    W/i.sc/l.sc/c.sc/o.sc/x.sc, J. R., W/o.sc/o.sc/s.sc, D., P/a.sc/n.sc/c.sc/h.sc/e.sc/k.sc/h.sc/a.sc, P., T/a.sc/t.sc/l.sc/o.sc/c.sc/k.sc, Z., W /a.sc/n.sc/g.sc, X., E/r.sc/n.sc/s.sc/t.sc, M. D., /a.sc/n.sc/d.sc A/n.sc/d.sc/e.sc/r.sc/s.sc/o.sc/n.sc, T. E.Verdi: a framework for implementing and formally verifying distributed systems. In Proceedings of the 36...

    work page 2015

  46. [46]

    R., A/n.sc/t.sc/o.sc/n.sc, S., T/a.sc/t.sc/l.sc/o.sc/c.sc/k.sc, Z., E/r.sc/n.sc/s.sc/t.sc, M

    W/o.sc/o.sc/s.sc, D., W/i.sc/l.sc/c.sc/o.sc/x.sc, J. R., A/n.sc/t.sc/o.sc/n.sc, S., T/a.sc/t.sc/l.sc/o.sc/c.sc/k.sc, Z., E/r.sc/n.sc/s.sc/t.sc, M. D.,/a.sc/n.sc/d.sc A/n.sc/d.sc/e.sc/r.sc/s.sc/o.sc/n.sc, T.Planning for Change in a Formal Verification of the Raft Consensus Protocol. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Pr ograms and ...

    work page 2016

  47. [47]

    In 16th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2022, Carlsbad, CA, USA, July 11-13, 2022 (2022), M

    Y /a.sc/o.sc, J., T/a.sc/o.sc, R., G/u.sc, R., /a.sc/n.sc/d.sc N/i.sc/e.sc/h.sc, J.DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols. In 16th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2022, Carlsbad, CA, USA, July 11-13, 2022 (2022), M. K. Aguilera and H. Weatherspoon, Eds., USENIX Ass...

    work page 2022

  48. [48]

    In 15th USENIX Symposium on Operating Systems Design and Imple mentation (OSDI 21) (July 2021), USENIX Association, pp

    Y /a.sc/o.sc, J., T/a.sc/o.sc, R., G/u.sc, R., N/i.sc/e.sc/h.sc, J., J/a.sc/n.sc/a.sc, S., /a.sc/n.sc/d.sc R/y.sc/a.sc/n.sc, G.DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In 15th USENIX Symposium on Operating Systems Design and Imple mentation (OSDI 21) (July 2021), USENIX Association, pp. 405–421

    work page 2021

  49. [49]

    In Correct Hardware Design and Verifi- cation Methods (Berlin, Heidelberg, 1999), L

    Y/u.sc, Y., M/a.sc/n.sc/o.sc/l.sc/i.sc/o.sc/s.sc, P., /a.sc/n.sc/d.sc L/a.sc/m.sc/p.sc/o.sc/r.sc/t.sc, L.Model Checking TLA+ Specifications. In Correct Hardware Design and Verifi- cation Methods (Berlin, Heidelberg, 1999), L. Pierre and T. Kropf, Eds., Springer B erlin Heidelberg, pp. 54–66. , Vol. 1, No. 1, Article . Publication date: April 2024

    work page 1999