Verification of ThresholdBased Distributed Algorithms by Decomposition to Decidable Logics
Abstract
Verification of faulttolerant distributed protocols is an immensely difficult task. Often, in these protocols, thresholds on set cardinalities are used both in the process code and in its correctness proof, e.g., a process can perform an action only if it has received an acknowledgment from at least half of its peers. Verification of thresholdbased protocols is extremely challenging as it involves two kinds of reasoning: firstorder reasoning about the unbounded state of the protocol, together with reasoning about sets and cardinalities. In this work, we develop a new methodology for decomposing the verification task of such protocols into two decidable logics: EPR and BAPA. Our key insight is that such protocols use thresholds in a restricted way as a means to obtain certain properties of “intersection” between sets. We define a language for expressing such properties, and present two translations: to EPR and BAPA. The EPR translation allows verifying the protocol while assuming these properties, and the BAPA translation allows verifying the correctness of the properties. We further develop an algorithm for automatically generating the properties needed for verifying a given protocol, facilitating fully automated deductive verification. Using this technique we have verified several challenging protocols, including Byzantine onestep consensus, hybrid reliable broadcast and fast Byzantine Paxos.
1 Introduction
Faulttolerant distributed protocols play an important role in the avionic and automotive industries, medical devices, cloud systems, blockchains, etc. Their unexpected behavior might put human lives at risk or cause a huge financial loss. Therefore, their correctness is of ultimate importance.
Ensuring correctness of distributed protocols is a notoriously difficult task, due to the unbounded number of processes and messages, as well as the nondeterministic behavior caused by the presence of faults, concurrency, and message delays. In general, the problem of verifying such protocols is undecidable. This imposes two directions for attacking the problem: (i) developing fullyautomatic verification techniques for restricted classes of protocols, or (ii) designing deductive techniques for a wide range of systems that require user assistance. Within the latter approach, recently emerging techniques [29] leverage decidable logics that are supported by mature automated solvers to significantly reduce user effort, and increase verification productivity. Such logics bring several key benefits: (i) their solvers usually enjoy stable performance, and (ii) whenever annotations provided by the user are incorrect, the automated solvers can provide a counterexample for the user to examine.
Deductive verification based on decidable logic requires a logical formalism that satisfies two conflicting criteria: the formalism should be expressive enough to capture the protocol, its correctness properties, its inductive invariants, and ultimately its verification conditions. At the same time, the formalism should be decidable and have an effective automated tool for checking verification conditions.
In this paper we develop a methodology for deductive verification of thresholdbased distributed protocols using decidable logic, wellestablished decidable logics to settle the tension explained above.
In thresholdbased protocols, a process may take different actions based on the number of processes from which it received certain messages. This is often used to achieve faulttolerance. For example, a process may take a certain step once it has received an acknowledgment from a strict majority of its peers, that is, from more than \(\mathbf{n}/2\) processes, where \(\mathbf{n}\) is the total number of processes. Such expressions as \(\mathbf{n}/2\), are called thresholds, and in general they can depend on additional parameters, such as the maximal number of crashed processes, or the maximal number of Byzantine processes.
Verification of such protocols requires two flavors of reasoning, as demonstrated by the following example. Consider the Paxos [20] protocol, in which each process proposes a value and all must agree on a common proposal. The protocol tolerates up to \(\mathbf{t}\) process crashes, and ensures that every two processes that decide agree on the decided value. The protocol requires \(\mathbf{n}>2\mathbf{t}\) processes, and each process must obtain confirmation messages from \(\mathbf{n}\mathbf{t}\) processes before making a decision. The protocol is correct due to, among others, the fact that if \(\mathbf{n}>2\mathbf{t}\) then any two sets of \(\mathbf{n}\mathbf{t}\) processes have a process in common. To verify this protocol we need to express (i) relationships between an unbounded number of processes and values, which typically requires quantification over uninterpreted domains (“every two processes”), and (ii) properties of sets of certain cardinalities (“any two sets of \(\mathbf{n}\mathbf{t}\) processes intersect”). Crucially, these two types of reasoning are intertwined, as the sets of processes for which we need to capture cardinalities may be defined by their relations with other state components (“messages from at least \(\mathbf{n}\mathbf{t}\) processes”). While uninterpreted firstorder logic (FOL) seems like the natural fit for the first type of reasoning, it is seemingly a poor fit for the second type, since it cannot express set cardinalities and the arithmetic used to define thresholds. Typically, logics that combine both types of reasoning are either undecidable or not flexible enough to capture protocols as intricate as the ones we consider.
The approach we present relies on the observation that thresholdbased protocols and their correctness proofs use set cardinality thresholds in a restricted way as a means to obtain certain properties between sets, and that these properties can be expressed in FOL via a suitable encoding. In the example above, the important property is that every two sets of cardinality at least \(\mathbf{n}\mathbf{t}\) have a nonempty intersection. This property can be encoded in FOL by modeling sets of cardinality at least \(\mathbf{n}\mathbf{t}\) using an uninterpreted sort along with a membership relation between this sort and the sort for processes. However, the validity of the property under the assumption that \(\mathbf{n}> 2\mathbf{t}\) cannot be verified in FOL.
The key idea of this paper is, hence, to decompose the verification problem of thresholdbased protocols into the following problems: (i) Checking protocol correctness assuming certain intersection properties, which can be reduced to verification conditions expressed in the Effectively Propositional (EPR) fragment of FOL [25, 35]. (ii) Checking that sets with cardinalities adhering to the thresholds satisfy the intersection properties (under the protocol assumptions), which can be reduced to validity checks in quantifierfree Boolean Algebra with Presburger Arithmetic (BAPA) [19]. Both BAPA and EPR are decidable logics, and are supported by mature solvers.
A crucial step in employing this decomposition is finding suitable intersection properties that are strong enough to imply the protocol’s correctness (i.e., imply the FOL verification conditions), and are also implied by the precise definitions of the thresholds and the protocol’s assumptions. Thus, these intersection properties can be viewed as interpolants between the FOL verification conditions and the thresholds in the context of the protocol’s assumptions. We present fully automated procedures to find such intersection property interpolants, either eagerly or lazily.
 1.
We define a threshold intersection property (TIP) language for expressing properties of sets whose cardinalities adhere to certain thresholds; TIP is expressive enough to capture the properties required to prove the correctness of challenging thresholdbased protocols.
 2.
We develop two encodings of TIP, one in BAPA, and another in EPR. These encodings facilitate decomposition of protocol verification into decidable EPR and (quantifierfree) BAPA queries.
 3.
We show that there are only finitely many TIP formulas (up to equivalence) that are valid for any given protocol. Moreover, we present an effective algorithm for computing all TIP formulas valid for a given protocol, as well as an algorithm for lazily finding a set of TIP formulas that suffice to prove a given protocol.
 4.
Put together, we obtain an effective deductive verification approach for thresholdbased protocols: the user models the protocol and its inductive invariants in EPR using a suitable encoding of thresholds, and defines the thresholds and the protocol’s assumptions using arithmetic; verification is carried out automatically via decomposition to wellestablished decidable logics.
 5.
We implement the approach, leveraging mature existing solvers (Z3 and CVC4), and evaluate it by verifying several challenging thresholdbased protocols with sophisticated thresholds and assumptions. Our evaluation shows the effectiveness and flexibility of our approach in modeling and verifying complex protocols, including the feasibility of automatically inferring threshold intersection properties.
2 Preliminaries
Transition Systems in FOL. We model distributed protocols as transition systems expressed in manysorted FOL. A state of the system is a firstorder (FO) structure \(s= ({\mathcal {D}}, {\mathcal {I}})\) over a vocabulary \(\varSigma \) that consists of sorted constant, function and relation symbols, s.t. \(s\) satisfies a finite set of axioms \(\varTheta \) in the form of closed formulas over \(\varSigma \). \({\mathcal {D}}\) is the domain of \(s\) mapping each sort to a set of objects (elements), and \({\mathcal {I}}\) is the interpretation function. A FO transition system is a tuple \((\varSigma , \varTheta , I, \textit{TR})\), where \(\varSigma \) and \(\varTheta \) are as above, \(I\) is a closed formula over \(\varSigma \) that defines the initial states, and \(\textit{TR}\) is a closed formula over \(\varSigma \uplus \varSigma '\) that defines the transition relation where \(\varSigma \) describes the source state of a transition and \(\varSigma ' = \{a' \mid a \in \varSigma \}\) describes the target state. We require that \(\textit{TR}\) does not modify any symbol that appears in \(\varTheta \). The set of reachable states is defined as usual. In practice, we define FO transition systems using a modeling language with a convenient syntax [29].
Properties and Inductive Invariants. A safety property is expressed by a closed FO formula \(P\) over \(\varSigma \). The system is safe if all of its reachable states satisfy \(P\). A closed FO formula \(\textit{Inv}\) over \(\varSigma \) is an inductive invariant for a transition system \((\varSigma , \varTheta , I, \textit{TR})\) and property \(P\) if the following formulas, called the verification conditions, are valid (equivalently, their negations are unsatisfiable): (i) \(\varTheta \rightarrow (I\rightarrow \textit{Inv})\), (ii) \(\varTheta \rightarrow (\textit{Inv}\wedge \textit{TR}\rightarrow \textit{Inv}')\) and (iii) \(\varTheta \rightarrow (\textit{Inv}\rightarrow P)\), where \(\textit{Inv}'\) results from substituting every symbol in \(\textit{Inv}\) by its primed version. We also use inductive invariants to verify arbitrary firstorder LTL formulas via the reduction of [30, 31].
Effectively Propositional Logic (EPR). The effectivelypropositional (EPR) fragment of FOL is restricted to formulas without function symbols and with a quantifier prefix \(\exists ^* \forall ^*\) in prenex normal form. Satisfiability of EPR formulas is decidable [25]. Moreover, EPR formulas enjoy the finite model property, i.e., \(\varphi \) is satisfiable iff it has a finite model. We consider a straightforward extension of EPR that maintains these properties and is supported by solvers such as Z3 [5]. The extension allows function symbols and quantifier alternations as long as the formula’s quantifier alternation graph, denoted \(\textit{QA}(\varphi )\), is acyclic. For \(\varphi \) in negation normal form, \(\textit{QA}(\varphi )\) is a directed graph where the set of vertices is the set of sorts and the set of edges is defined as follows: every function symbol introduces edges from its arguments’ sorts to its image’s sort, and every existential quantifier \(\exists x\) that resides in the scope of universal quantifiers introduces edges from the sorts of the universally quantified variables to the sort of x. The quantifier alternation graph is extended to sets of formulas as expected.
A BAPA structure is \(s_B= ({\mathcal {D}}, {\mathcal {I}})\) where the domain \({\mathcal {D}}\) maps sort \(\mathsf {int}\) to the set of all integers and maps sort \(\mathsf {set}\) to the set of all subsets of a finite universe U, called the universal set. The semantics of terms and formulas is as expected, where the interpretation of the complement operation is defined with respect to U (e.g., \({\mathcal {I}}(\emptyset ^c) = U\)), and the integer constant \(\mathbf{n}\) is interpreted to the size of U, i.e. \({\mathcal {I}}(\mathbf{n}) = {\left {U}\right }\).
Both validity and satisfiability of BAPA formulas (with arbitrary quantification) are decidable [19], and the quantifierfree fragment is supported by CVC4 [2].
3 FirstOrder Modeling of ThresholdBased Protocols
Running Example. We illustrate our approach using the example of Bosco—an asynchronous Byzantine faulttolerant (BFT) consensus algorithm [39]. Its modeling in firstorder logic using our technique appears alongside an informal pseudocode in Fig. 1.
In the BFT consensus problem, each node proposes a value and correct nodes must decide on a unique proposal. BFT consensus algorithms typically require at least two communication rounds to reach a decision. In Bosco, nodes execute a preliminary communication step which, under favorable conditions, reaches an early decision, and then call an underlying BFT consensus algorithm to ensure reaching a decision even if these conditions are not met. Bosco is safe when \(\mathbf{n}> 3\mathbf{t}\); it guarantees that a preliminary decision will be reached if all nodes are nonfaulty and propose the same value when \(\mathbf{n}> 5\mathbf{t}\) (weakly onestep condition), and even if some nodes are faulty, as long as all nonfaulty nodes propose the same value, when \(\mathbf{n}> 7\mathbf{t}\) (strongly onestep condition).
Bosco achieves consensus by ensuring that (a) no two correct nodes decide differently in the preliminary step, and (b) if a correct node decides value v in the preliminary step then every correct process calls the underlying BFT consensus algorithm with proposal v. Property (a) is ensured by the fact that a node decides in the preliminary step only if more than \(\frac{\mathbf{n}+3\mathbf{t}}{2}\) nodes proposed the same value. When \(\mathbf{n}>3\mathbf{t}\), two sets of cardinality greater than \(\frac{\mathbf{n}+3\mathbf{t}}{2}\) have at least one nonfaulty node in common, and therefore no two different values can be proposed by more than \(\frac{\mathbf{n}+3\mathbf{t}}{2}\) nodes. Similarly, we can derive property (b) from the fact that a set of more than \(\frac{\mathbf{n}+3\mathbf{t}}{2}\) nodes and a set of \(\mathbf{n}\mathbf{t}\) nodes intersect in \(\frac{\mathbf{n}+\mathbf{t}}{2}\) nodes, which, after removing t nodes which may be faulty, still leaves us with more than \(\frac{\mathbf{n}\mathbf{t}}{2}\) nodes, satisfying the condition in line 9.
3.1 ThresholdBased Protocols
Parameters and Resilience Conditions. We consider protocols whose definitions depend on a set of parameters, \(\textit{Prm}\), divided into integer parameters, \(\textit{Prm}_{I}\), and set parameters, \(\textit{Prm}_{S}\). \(\textit{Prm}_{I}\) always includes \(\mathbf{n}\), the total number of nodes (assumed to be finite). Protocol correctness is ensured under a set of assumptions \(\varGamma \) called resilience conditions, formulated as BAPA formulas over \(\textit{Prm}\) (this means that all the uninterpreted constants appearing in \(\varGamma \) are from \(\textit{Prm}\)). In Bosco, \(\textit{Prm}_{I}= \{\mathbf{n}, \mathbf{t}\}\), where \(\mathbf{t}\) is the maximal number of Byzantine failures tolerated by the algorithm, and \(\textit{Prm}_{S}= \{ \mathbf{f}\}\), where \(\mathbf{f}\) is the set of Byzantine nodes; \(\varGamma = \{ \mathbf{n}\ge 3 \mathbf{t}+ 1, {\left {\mathbf{f}}\right } \le \mathbf{t}\}\).
Threshold Conditions. Both the description of the protocol and the inductive invariant may include conditions that require the size of some set of nodes to be “at least t”, “at most t”, and so on, where the threshold t is of the form \(t=\frac{\ell }{k}\), where k is a positive integer, and \(\ell \) is a ground BAPA integer term over \(\textit{Prm}\) (we do not allow comparing sizes of two sets – we observe that it is not needed for thresholdbased protocols). We denote the set of thresholds by \(T\). For example, in Bosco, \(T= \{ \mathbf{n} \mathbf{t}, \frac{\mathbf{n}+ 3 \mathbf{t}+ 1}{2}, \frac{\mathbf{n} \mathbf{t}+ 1}{2} \}\).
3.2 Modeling in FOL

For every threshold t we introduce a threshold sort \(\mathsf {set}_{\mathsf {t}}\) with the intended meaning that elements of this sort are sets of nodes whose size is at least t.

Each sort \(\mathsf {set}_{\mathsf {t}}\) is equipped with a binary relation symbol \({\textit{member}}_{t}\) between sorts \(\mathsf {node}\) and \(\mathsf {set}_{\mathsf {t}}\) that captures the membership relation of a node in a set.

For each set parameter \(\mathbf{a}\in \textit{Prm}_{S}\) we introduce a unary relation symbol \({\textit{member}}_{\mathbf{a}}\) over sort \(\mathsf {node}\) that captures membership of a node in the set \(\mathbf{a}\).
We then model the protocol as a transition system \((\varSigma , \varTheta , I, \textit{TR})\) where \(\varSigma =\varSigma _C\uplus \varSigma _{T}^{\textit{Prm}}\).
We are interested only in states (FO structures over \(\varSigma \)) where the interpretation of the threshold sorts and membership relations is according to their intended meaning in a corresponding BAPA structure. Formally, these are \(T\)extensions, defined as follows:
Definition 1
Note that for the \(T\)extension \(s\) to be well defined as a FO structure, we must have that \({\mathcal {D}}(\mathsf {set}_{\mathsf {t}}) \ne \emptyset \) for every threshold \(t \in T\). This means that a \(T\)extension by \(s_B\) only exists if \(\{A \subseteq {\mathcal {D}}(\mathsf {node}) \mid {\left {A}\right } \ge {\mathcal {I}}_B(t) \} \ne \emptyset \). This is ensured by the following condition:
Definition 2 (Feasibility)
\(T\) is \(\varGamma \)feasible if \(\varGamma \models t \le \mathbf{n}\) for every \(t \in T\).
Expressing Threshold Constraints. Cardinality constraints can be expressed in FOL over the vocabulary \(\varSigma =\varSigma _C\uplus \varSigma _{T}^{\textit{Prm}}\) using quantification. To express that \({\left {\{ n: \mathsf {node}\mid \varphi (n,\bar{u}) \}}\right } \ge t\), i.e., that there are at least t nodes that satisfy the FO formula \(\varphi \) over \(\varSigma _C\) (where \(\bar{u}\) are free variables in \(\varphi \)), we use the following firstorder formula over \(\varSigma \): \(\exists q : \mathsf {set}_{\mathsf {t}}. \; \forall n: \mathsf {node}. \; {\textit{member}}_t(n,q) \rightarrow \varphi (n,\bar{u})\). Similarly, to express the property that a node is a member of a set parameter \(\mathbf{a}\) (e.g., to check if \(n\in \mathbf{f}\), i.e., a node is faulty) we use the FO formula \({\textit{member}}_{\mathbf{a}}(n)\). For example, in Fig. 1, line 5 (right) uses the FO modeling to express the condition in line 5 (left). This modeling is sound in the following sense:
Lemma 1 (Soundness)
 1.
For every \(\mathbf{a}\in \textit{Prm}_{S}\) and FO valuation \(\iota \): \(s, \iota \models {\textit{member}}_{\mathbf{a}}(n)\) iff \(\iota (n) \in {\mathcal {I}}_B(\mathbf{a})\),
 2.
For every \(t \in T\), formula \(\varphi \), and FO valuation \(\iota \): \(s, \iota \models \exists q : \mathsf {set}_{\mathsf {t}}. \; \forall n: \mathsf {node}. \; {\textit{member}}_t(n,q) \rightarrow \varphi (n,\bar{u})\) iff \({\left {\{ e \in {\mathcal {D}}(\mathsf {node}) \mid s_C,\iota [n\mapsto e] \models \varphi (n,\bar{u}) \}}\right } \ge {\mathcal {I}}_B(t)\).
Definition 3
A firstorder structure \(s\) over \(\varSigma \) is thresholdfaithful if it is a \(T\)extension of some \(s_C\) by some \(s_B\models \varGamma \) (as in Lemma 1).
Incompleteness. Lemma 1 ensures that the FO modeling can be soundly used to verify the protocol. It also ensures that the modeling is precise on thresholdfaithful structures (Def. 1). Yet, the FO transition system is not restricted to such states, hence it abstracts the actual protocol. To have any hope to verify the protocol, we must capture some of the intended meaning of the threshold sorts and relations. This is obtained by adding FO axioms to the FO transition system. Soundness is maintained as long as the axioms hold in all thresholdfaithful structures. We note that the set of all such axioms is not recursively enumerable– this is where the essential incompleteness of our approach lies.
4 Decomposition via Threshold Intersection Properties
In this section, we identify a set of properties we call threshold intersection properties. When captured via FO axioms, these properties suffice for verifying many thresholdbased protocols (all the ones we considered). Importantly, these are properties of sets adhering to the thresholds that do not involve the protocol state. As a result, they can be expressed both in FOL and in BAPA. This allows us to decompose the verification task into: (i) checking that certain threshold properties are valid in all thresholdfaithful structures by checking that they are implied by \(\varGamma \) (carried out using quantifier free BAPA), and (ii) checking that the verification conditions of the FO transitionsystem with the same threshold properties taken as axioms are valid (carried out in firstorder logic, and in EPR if quantifier alternations are acyclic).
4.1 Threshold Intersection Property Language
Threshold properties are expressed in the threshold intersection property language (TIP). TIP is essentially a subset of BAPA, specialized to have the properties listed above.
Example 1
If \(\varGamma \) is quantifierfree (which is the typical case), \(\varGamma \)validity of TIP formulas can be checked via validity checks of quantifierfree BAPA formulas, supported by mature solvers. Note that \(\varGamma \)validity of a formula of the form \(\forall x:g_{\ge t_1}.\ {\left {x \cap b}\right } \ge t_2\) is equivalent to \(\varGamma \models \forall u.\ u \ge t_1 \rightarrow u + {\left {b}\right } n \ge t_2\), allowing replacing quantification over sets by quantification over integers, thus improving performance of existing solvers.
4.2 Translation to FOL
We lift \(\mathcal {FO}\) to sets of formulas: \(\mathcal {FO}(\varDelta ) = \{\mathcal {FO}(\varphi ) \mid \varphi \in \varDelta \}\).
Next, we state the soundness of the translation, which intuitively means that \(\mathcal {FO}(\varphi )\) is “equivalent” to \(\varphi \) over thresholdfaithful FO structures (Definition 1). This justifies adding \(\mathcal {FO}(\varphi )\) as a FO axiom whenever \(\varphi \) is \(\varGamma \)valid.
Theorem 1 (Translation soundness)
Let \(s_C= ({\mathcal {D}}_C, {\mathcal {I}}_C)\) be a firstorder structure over \(\varSigma _C\), \(s_B= ({\mathcal {D}}_B, {\mathcal {I}}_B)\) a compatible BAPA structure over \(\textit{Prm}\), and \(s\) the \(T\)extension of \(s_C\) by \(s_B\). Then for every closed TIP formula \(\varphi \), we have \(s_B\models \varphi \Leftrightarrow s\models \mathcal {FO}(\varphi ).\)
Corollary 1
For every closed TIP formula \(\varphi \) such that \(\varGamma \models \varphi \), we have that \(\mathcal {FO}(\varphi )\) is satisfied by every thresholdfaithful firstorder structure.
5 Automatically Inferring Threshold Intersection Properties
To apply the approach described in Sects. 3 and 4, it is crucial to find suitable threshold properties. That is, given the resilience conditions \(\varGamma \) and a FO transition system modeling the protocol, we need to find a set \(\varDelta \) of TIP formulas such that (i) \(\varGamma \models \varphi \) for every \(\varphi \in \varDelta \), and (ii) the VCs of the transition system with the axioms \(\mathcal {FO}(\varDelta )\) are valid.
In this section, we address the problem of automatically inferring such a set \(\varDelta \). In particular, we prove that for any protocol that satisfies a natural condition, there are finitely many \(\varGamma \)valid TIP formulas (up to equivalence), enabling a complete automatic inference algorithm. Furthermore, we show that (under certain reasonable conditions formalized in this section), the FO axioms resulting from the inferred TIP properties have an acyclic quantifier alternation graph, facilitating protocol verification in EPR.
Notation. For the rest of this section, we fix a set \(\textit{Prm}\) of parameters, a set \(\varGamma \) of resilience conditions over \(\textit{Prm}\), and a set \(T\) of thresholds. Note that \(b\ne \emptyset \equiv g_{\ge 1}(b)\) and \(b^c = \emptyset \equiv g_{\ge \mathbf{n}}(b)\). Therefore, for uniformity of the presentation, given a set \(T\) of thresholds, we define \(\hat{T}\buildrel {\tiny \mathrm def} \over =T\cup \{1, \mathbf{n}\}\) and replace atomic formulas of the form \(b\ne \emptyset \) and \(b^c = \emptyset \) by the corresponding guard formulas. As such, the only atomic formulas are of the form \(g_{\ge t}(b)\) where \(t \in \hat{T}\). Note that guards in quantifiers are still restricted to \(g_{\ge t}\) where \(t \in T\). Given a set \(\textit{Prm}_{S}\), we also denote \(\hat{\textit{Prm}_{S}} = \textit{Prm}_{S}\cup \{\mathbf{a}^c \mid \mathbf{a}\in \textit{Prm}_{S}\}\).
5.1 Finding Consequences in the Threshold Intersection Property Language
In this section, we present Aip– an algorithm for inferring all \(\varGamma \)valid TIP formulas. A naïve (nonterminating) algorithm would iteratively check \(\varGamma \)validity of every TIP formula. Instead, Aip prunes the search space relying on the following condition:
Definition 4
\(T\) is \(\varGamma \)nondegenerate if for every \(t \in T\) it holds that \(\varGamma \not \models t \le 0\).
If \(\varGamma \models t \le 0\) then t is degenerate in the sense that \(g_{\ge t}(b)\) is always \(\varGamma \)valid, and \(\forall x: g_{\ge t}. \ g_{\ge t'}(x \cap b)\) is never \(\varGamma \)valid unless \(t'\) is also degenerate.
We observe that we can (i) push conjunctions outside of formulas (since \(\forall \) distributes over \(\wedge \)), and assuming nondegeneracy, (ii) ignore terms of the form \(x^c\):
Lemma 2
We refer to \(\varphi _i\) of the form above as simple, and refer to \(g_{\ge t}\) as its atomic guard.
By Lemma 2, it suffices to generate all simple \(\varGamma \)valid formulas. Next, we show that this can be done more efficiently by pruning the search space based on a subsumption relation that is checked syntactically avoiding \(\varGamma \)validity checks.
Definition 5 (Subsumption)
For every \(h_1, h_2 \in \hat{T}\cup \hat{\textit{Prm}_{S}}\), we denote \(h_1 \sqsubseteq _\varGamma h_2\) if one of the following holds: (1) \(h_1 = h_2\), or (2) \(h_1, h_2 \in \hat{T}\) and \(\varGamma \models h_1 \ge h_2\), or (3) \(h_1 \in \hat{\textit{Prm}_{S}}\), \(h_2 \in \hat{T}\) and \(\varGamma \models {\left {h_1}\right } \ge h_2\).
For \(h_1,h_2 \in \hat{T}\) and \(h_3 \in \hat{\textit{Prm}_{S}}\), \(h_1 \sqsubseteq _\varGamma h_2\) means that \(\varGamma \models \forall x:g_{\ge h_1}.\ g_{\ge h_2}(x)\), and \(h_3 \sqsubseteq _\varGamma h_2\) means that \(\varGamma \models g_{\ge h_2}(h_3)\). We lift the relation \(\sqsubseteq _\varGamma \) to act on simple formulas:
Definition 6
Lemma 3
Let \(\alpha , \beta \) be simple formulas such that \(\alpha \sqsubseteq _\varGamma \beta \). If \(\varGamma \models \alpha \) then \(\varGamma \models \beta \).
Corollary 2
If no simple formula with q quantifiers is \(\varGamma \)valid then no simple formula with more than q quantifiers is \(\varGamma \)valid.
Lemma 4 (Soundness)
Every formula \(\varphi \) that is returned by the algorithm is \(\varGamma \)valid.
Lemma 5 (Completeness)
If \(T\) is \(\varGamma \)feasible and \(\varGamma \)nondegenerate, then for every \(\varGamma \)valid TIP formula \(\varphi \) there exist \(\varphi _1\ldots \varphi _m\) s.t. \(\varphi \equiv \bigwedge _{i=1}^m \varphi _i\) and \(\textsc {Aip} \) yields every \(\varphi _i\).
Next, we characterize the cases in which there are finitely many \(\varGamma \)valid TIP formulas, up to equivalence, and thus, Aip is guaranteed to terminate.
Definition 7
\(T\) is \(\varGamma \)sane if for every \(t_1, t_2 \in T\), \(\varGamma \not \models t_1 \le 0 \vee t_2 > \mathbf{n} 1\). \((T,\textit{Prm}_{S})\) is \(\varGamma \)sane if, in addition, for every \(t_1 \in T\), \(a \in \hat{\textit{Prm}_{S}}\), \(\varGamma \not \models t_1 \le 0 \vee {\left {a}\right } = \mathbf{n}\).
Theorem 2
Assume that \(T\) is \(\varGamma \)feasible. Then the following conditions are equivalent: (1) There are finitely many \(\varGamma \)valid simple formulas. (2) There are finitely many \(\varGamma \)valid TIP formulas, up to equivalence. (3) \(T\) is \(\varGamma \)sane.
Corollary 3 (Termination)
If \(T\) is \(\varGamma \)feasible and \(\varGamma \)sane, Aip terminates.
5.2 From TIP to Axioms in EPR
The set of simple formulas generated by Aip, \(\varDelta \), is translated to FOL axioms as described in Sect. 4.2. Next, we show how to ensure that the quantifier alternation graph (Sect. 2) of \(\mathcal {FO}(\varDelta )\) is acyclic. A simple formula induces quantifier alternation edges in \(\textit{QA}(\mathcal {FO}(\varphi ))\) from the sorts of its universal quantifiers to the sort of its atomic guard \(g_{\ge t}\) (or if \(t = 1\) to the \(\mathsf {node}\) sort). Therefore, from Lemma 3, for a \(\varGamma \)valid \(\varphi \), cycles in \(\textit{QA}(\mathcal {FO}(\varphi ))\) may only occur if they occur in the graph obtained by \(\sqsubseteq _\varGamma \). Furthermore, if \(\textit{QA}(\mathcal {FO}(\varphi ))\) is not acyclic, then the atomic guard must be equal to one of the quantifier guards. We refer to such a formula as a cyclic formula. We show that, under the following assumption, we can eliminate all cyclic formulas from \(\varDelta \).
Definition 8
\(T\) is \(\varGamma \)acyclic if for every \(t_1,t_2 \in T\), if \(\varGamma \models t_1 = t_2\) then \(t_1 = t_2\).
Intuitively, if \(T\) is not \(\varGamma \)acyclic, then it has (at least) two “equivalent” thresholds, making one of them redundant. If that is the case, we can alter the protocol and its proof so that one of these guards is eliminated and the other one is used instead.
Theorem 3
Let \(T\) be \(\varGamma \)feasible and \(\varGamma \)acyclic and \((T,\textit{Prm}_{S})\) be \(\varGamma \)sane. Let \(\varDelta \) be the set returned by Aip, and Open image in new window . Then the VCs of the FO transition system with axioms \(\mathcal {FO}(\varDelta )\) are valid iff they are valid with axioms \(\mathcal {FO}(\varDelta ')\). Further, \(\textit{QA}(\mathcal {FO}(\varDelta '))\) is acyclic.
5.3 Finding Minimal Properties Required for a Protocol
If \(\varDelta \) consists of all acyclic \(\varGamma \)valid TIP formulas returned by Aip, using \(\mathcal {FO}(\varDelta )\) as FO axioms leads to divergence of the verifier. To overcome this, we propose two variants.
Minimal Equivalent. \(\varDelta _{min}\). Some of the formulas in \(\mathcal {FO}(\varDelta )\) are implied by others, making them redundant. We remove such formulas using a greedy procedure that for every \(\varphi _i \in \varDelta \), checks whether \(\mathcal {FO}(\varDelta \setminus \{\varphi _i\}) \models \mathcal {FO}(\varphi _i)\), and if so, removes \(\varphi _i\) from \(\varDelta \). Note that if \(\textit{QA}(\mathcal {FO}(\varDelta ))\) is acyclic, the check translates to (un)satisfiability in EPR.
This procedure results in \(\varDelta _{min} \subseteq \varDelta \) s.t. \(\mathcal {FO}(\varDelta _{min}) \models \mathcal {FO}(\varDelta )\) and no strict subset of \(\varDelta _{min}\) satisfies this condition. That is, \(\varDelta _{min}\) is a local minimum for that property.
Interpolant. \(\varDelta _{int}\). There may exist \(\varDelta _{int} \subseteq \varDelta \) s.t. \(\mathcal {FO}(\varDelta _{int}) \not \models \mathcal {FO}(\varDelta )\) but \(\mathcal {FO}(\varDelta _{int})\) suffices to prove the firstorder VCs, and enables to discharge the VCs more efficiently. We compute such a set \(\varDelta _{int}\) iteratively. Initially, \(\varDelta _{int}= \emptyset \). In each iteration, we check the VCs. If a counterexample to induction (CTI) is found, we add to \(\varDelta _{int}\) a formula from \(\varDelta \) not satisfied by the CTI. In this approach, \(\varDelta \) is not precomputed. Instead, Aip is invoked lazily to generate candidate formulas in reaction to CTIs.
6 Evaluation
We evaluate the approach by verifying several challenging thresholdbased distributed protocols that use sophisticated thresholds: we verify the safety of Bosco [39] (presented in Sect. 3) under its 3 different resilience conditions, the safety and liveness (using the liveness to safety reduction presented in [30]) of Hybrid Reliable Broadcast [40], and the safety of Byzantine Fast Paxos [23]. Hybrid Reliable Broadcast tolerates four different types of faults, while Fast Byzantine Paxos is a fastlearning [21, 22] Byzantine faulttolerant consensus protocol; fastlearning protocols are notorious because two such algorithms, Zyzzyva [17] and FaB [28], were recently revealed incorrect [1] despite having been published at major systems conferences.
Figure 2 lists the protocols we verified and the details of the evaluation. Each experiment was repeated 10 times, and we report the mean time (\(\mu \)) and standard deviation (\(\sigma \)). The figure’s caption explains the presented information, and we discuss the results below.
Aip\(_\textsc {Eager}\) For all protocols, running Aip took less than 1 min (column \(\mathbf {t_C}\)), and generated all \(\varGamma \)valid simple TIP formulas. We observe that for most formulas, (in)validity is deduced from other formulas by subsumption, and less than 2%–5% of the formulas are actually checked using a BAPA query. With the optimization of the redundancy check, minimization of the set is performed in negligible time. The resulting set, \(\varDelta _\textsc {Eager}\), contains 3–5 formulas, compared to 39–79 before minimization.
Due to the optimization described in Sect. 4 for the BAPA validity queries, the number of quantifiers in the TIP formulas that are checked by Aip does not affect the time needed to compute the full \(\varDelta \). For example, Bosco under the Strongly Onestep resilience condition contains \(\varGamma \)valid simple TIP formulas with up to 7 quantifiers (as \(\mathbf{n}> 7\mathbf{t}\) and \(t_1 = \mathbf{n} \mathbf{t}\)), but \(\textsc {Aip} \) does not take significantly longer to find \(\varDelta \). Interestingly, in this example the \(\varGamma \)valid TIP formulas with more than 3 quantifiers are implied (in FOL) by formulas with at most 3 quantifiers, as indicated by the fact that these are the only formulas that remain in \(\varDelta _\textsc {Eager}^{\text {Bosco Strongly Onestep}}\).
Aip\(_\textsc {Lazy}\) With the lazy approach based on CTIs, the time for finding the set of TIP formulas, \(\varDelta _\textsc {Lazy}\), is generally longer. This is because the run time is dominated by calls to Ivy with FO axioms that are too weak for verifying the protocol. However, the resulting \(\varDelta _\textsc {Lazy}\) has a significant benefit: it lets Ivy prove the protocol much faster compared to using \(\varDelta _\textsc {Eager}\). Comparing \(\mathbf {t_V}\) in Aip \(_\textsc {Eager}\) vs. Aip \(_\textsc {Lazy}\) shows that when the former takes a minute, the latter takes a few seconds, and when the former times out after 1 h, the latter terminates, usually in under 1 min. Comparing the formulas of \(\varDelta _\textsc {Eager}\) and \(\varDelta _\textsc {Lazy}\) reveals the reason. While the FO translation of both yields EPR formulas, the formulas resulting from \(\varDelta _\textsc {Eager}\) contain more quantifiers and generate much more ground terms, which degrades the performance of Z3.
Another advantage of the lazy approach is that during the search, it avoids considering formulas with many quantifiers unless those are actually needed. Comparing the 3 versions of Bosco we see that Aip \(_\textsc {Lazy}\) is not sensitive to the largest number of quantifiers that may appear in a \(\varGamma \)valid simple TIP formula. The downside is that Aip \(_\textsc {Lazy}\) performs many Ivy checks in order to compute the final \(\varDelta _\textsc {Lazy}\). The total duration of finding CTIs varies significantly (as demonstrated under the column \(\mathbf {t_I}\)), in part because it is very sensitive to the CTIs returned by Ivy, which are in turn affected by the random seed used in the heuristics of the underlying solver.
Finally, \(\varDelta _\textsc {Lazy}\) provides more insight into the protocol design, since it presents minimal assumptions that are required for protocol correctness. Thus, it may be useful in designing and understanding protocols.
7 Related Work
Fully Automatic Verification of ThresholdBased Protocols. Algorithms modeled as Threshold automata (TA) [14] have been studied in [13, 16], and verified using an automated tool ByMC [15]. The tool also automatically synthesizes thresholds as arithmetic expressions [24]. Reachability properties of TAs for more general thresholds are studied in [18]. There have been recent advances in verification of synchronous thresholdbased algorithms using TAs [41], and of asynchronous randomized algorithms where TAs support coin tosses and an unbounded number of rounds [4]. Still, this modeling is very restrictive and not as faithful to the pseudocode as our modeling.
Another approach for full automation is to use sound and incomplete procedures for deduction and invariant search for logics that combine quantifiers and set cardinalities [8, 10]. However, distributed systems of the level of complexity we consider here (e.g., Byzantine Fast Paxos) are beyond the reach of these techniques.
Verification of Distributed Protocols Using Decidable Logics. Padon et al. [33] introduced an interactive approach for the safety verification of distributed protocols based on EPR using the Ivy [29] verification tool. Later works extended the approach to more complex protocols [32], their implementations [42], and liveness properties [30, 31]. Those works verified some threshold protocols using adhoc firstorder modeling and axiomatization of thresholdintersection properties, whereas we develop a systematic methodology. Moreover, the axioms were not mechanically verified, except in [42], where a simple intersection property—intersection of two sets with more than \(\frac{\mathbf{n}}{2}\) nodes—requires a proof by induction over \(\mathbf{n}\). The proof relies on a user provided induction hypothesis that is automatically checked using the FAU decidable fragment [9]. This approach requires user ingenuity even for a simple intersection property, and we expect that it would not scale to the more complex properties required for e.g. Bosco or Fast Byzantine Paxos. In contrast, our approach completely automates both verification and inference of thresholdintersection properties required to verify protocol correctness.
Dragoi et al. [6] propose a decidable logic supporting cardinalities, uninterpreted functions, and universal quantifiers for verifying consensus algorithms expressed in the partially synchronous HeardOf Model. As in this paper, the user is expected to provide an inductive invariant. The PSync framework [7] extends the approach to protocol implementations. Compared to our approach, the approach of Dragoi et al. is less flexible due to the specialized logic used and the restrictions of the HeardOf Model.
Our approach decomposes verification into EPR and BAPA. Piskac [34] presents a decidable logic that combines BAPA and EPR, with some restrictions. The verification conditions of the protocols we consider are outside the scope of this fragment since they include cardinality constraints in the scope of quantifiers. Furthermore, this logic is not supported by mature solvers. Instead of looking for a specialized logic per protocol, we rely on a decomposition which allows more flexibility.
Recently, [11] presented an approach for verifying asynchronous algorithms by reduction to synchronous verification. This technique is largely orthogonal and complementary to our approach, which is focused on the challenge of cardinality thresholds.
Verification using interactive theorem provers. We are not aware of works based on interactive theorem provers that verified protocols with complex thresholds as we do in this work (although doing so is of course possible). However, many works used interactive theorem provers to verify related protocols, e.g., [12, 27, 36, 37, 38, 43] (the most related protocols use either \(\frac{{n}}{{2}}\) or \(\frac{{2n}}{{3}}\) as the only thresholds, other protocols do not involve any thresholds). The downside of verification using interactive theorem provers is that it requires tremendous human efforts and skills. For example, the Verdi proof of Raft included 50,000 lines of proof in Coq for 500 lines of code [44].
8 Conclusion
This paper proposes a new deductive verification approach for thresholdbased distributed protocols by decomposing the verification problem into two wellestablished decidable logics, BAPA and EPR, thus allowing greater flexibility compared to monolithic approaches based on domainspecific, specialized logics. The user models their protocol in EPR, defines the thresholds and resilience conditions using arithmetic in BAPA, and provides an inductive invariant. An automatic procedure infers threshold intersection properties expressed in TIP that are both (1) sound w.r.t. the resilience conditions (checked in quantifierfree BAPA) and (2) sufficient to discharge the VCs (checked in EPR). Both logics are supported by mature solvers, and allow providing the user with an understandable counterexample in case verification fails.
Our evaluation, which includes notoriously tricky fastlearning consensus protocols, shows that threshold intersection properties are inferred in a matter of minutes. While this may be too slow for interactive use, we expect improvements such as memoization and parallelism to provide response times of a few seconds in an iterative, interactive setting. Another potential future direction is combining our inference algorithm with automated invariant inference algorithms.
Footnotes
Notes
Acknowledgements
We thank the anonymous referees for insightful comments which improved this paper. This publication is part of a project that has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No [759102SVIS] and [787367PaVeS]). The research was partially supported by Len Blavatnik and the Blavatnik Family foundation, the Blavatnik Interdisciplinary Cyber Research Center, Tel Aviv University, the Israel Science Foundation (ISF) under grant No. 1810/18, the United StatesIsrael Binational Science Foundation (BSF) grant No. 2016260 and the Austrian Science Fund (FWF) through Doctoral College LogiCS (W1255N23).
References
 1.Abraham, I., Gueta, G., Malkhi, D., Alvisi, L., Kotla, R., Martin, J.P.: Revisiting Fast Practical Byzantine Fault Tolerance (2017)Google Scholar
 2.Bansal, K., Reynolds, A., Barrett, C., Tinelli, C.: A new decision procedure for finite sets and cardinality constraints in SMT. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 82–98. Springer, Cham (2016). https://doi.org/10.1007/9783319402291_7CrossRefGoogle Scholar
 3.Berkovits, I., Lazić, M., Losa, G., Padon, O., Shoham, S.: Verification of thresholdbased distributed algorithms by decomposition to decidable logics. CoRR abs/1905.07805 (2019). http://arxiv.org/abs/1905.07805
 4.Bertrand, N., Konnov, I., Lazic, M., Widder, J.: Verification of Randomized Distributed Algorithms under RoundRigid Adversaries. HAL hal01925533, November 2018. https://hal.inria.fr/hal01925533
 5.de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/9783540788003_24CrossRefGoogle Scholar
 6.Drăgoi, C., Henzinger, T.A., Veith, H., Widder, J., Zufferey, D.: A logicbased framework for verifying consensus algorithms. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 161–181. Springer, Heidelberg (2014). https://doi.org/10.1007/9783642540134_10CrossRefGoogle Scholar
 7.Dragoi, C., Henzinger, T.A., Zufferey, D.: PSync: A partially synchronous language for faulttolerant distributed algorithms. In: Proceedings of the 43rd Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20–22, 2016, vol. 51, no. 1, pp. 400–415 (2016). https://dblp.unitrier.de/rec/bibtex/conf/popl/DragoiHZ16?q=speculative%20AQ4%20Byzantine%20fault%20tolerance
 8.Dutertre, B., Jovanović, D., Navas, J.A.: Verification of faulttolerant protocols with sally. In: Dutle, A., Muñoz, C., Narkawicz, A. (eds.) NFM 2018. LNCS, vol. 10811, pp. 113–120. Springer, Cham (2018). https://doi.org/10.1007/9783319779355_8CrossRefGoogle Scholar
 9.Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306–320. Springer, Heidelberg (2009). https://doi.org/10.1007/9783642026584_25CrossRefGoogle Scholar
 10.v. Gleissenthall, K., Bjørner, N., Rybalchenko, A.: Cardinalities and universal quantifiers for verifying parameterized systems. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, pp. 599–613. ACM (2016)Google Scholar
 11.von Gleissenthall, K., Kici, R.G., Bakst, A., Stefan, D., Jhala, R.: Pretend synchrony: synchronous verification of asynchronous distributed programs. PACMPL 3(POPL), 59:1–59:30 (2019). https://dl.acm.org/citation.cfm?id=3290372Google Scholar
 12.Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S.T.V., Zill, B.: Ironfleet: proving practical distributed systems correct. In: Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, 4–7 October 2015, pp. 1–17 (2015). https://doi.org/10.1145/2815400.2815428,
 13.Konnov, I., Lazic, M., Veith, H., Widder, J.: Para\(^2\): Parameterized path reduction, acceleration, and SMT for reachability in thresholdguarded distributed algorithms. Form. Methods Syst. Des. 51(2), 270–307 (2017). https://link.springer.com/article/10.1007/s1070301702974CrossRefGoogle Scholar
 14.Konnov, I., Veith, H., Widder, J.: On the completeness of bounded model checking for thresholdbased distributed algorithms: reachability. Inf. Comput. 252, 95–109 (2017)MathSciNetCrossRefGoogle Scholar
 15.Konnov, I., Widder, J.: ByMC: byzantine model checker. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11246, pp. 327–342. Springer, Cham (2018). https://doi.org/10.1007/9783030034245_22CrossRefGoogle Scholar
 16.Konnov, I.V., Lazic, M., Veith, H., Widder, J.: A short counterexample property for safety and liveness verification of faulttolerant distributed algorithms. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 18–20 January 2017, pp. 719–734 (2017)Google Scholar
 17.Kotla, R., Alvisi, L., Dahlin, M., Clement, A., Wong, E.: Zyzzyva: speculative Byzantine fault tolerance. SIGOPS Oper. Syst. Rev. 41(6), 45–58 (2007)CrossRefGoogle Scholar
 18.Kukovec, J., Konnov, I., Widder, J.: Reachability in parameterized systems: all flavors of threshold automata. In: CONCUR. LIPIcs, vol. 118, pp. 19:1–19:17. Schloss Dagstuhl  LeibnizZentrum fuer Informatik (2018)Google Scholar
 19.Kuncak, V., Nguyen, H.H., Rinard, M.: An algorithm for deciding BAPA: boolean algebra with presburger arithmetic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 260–277. Springer, Heidelberg (2005). https://doi.org/10.1007/11532231_20CrossRefGoogle Scholar
 20.Lamport, L.: The Parttime Parliament 16(2), 133–169 (1998–2005). https://doi.org/10.1145/279227.279229CrossRefGoogle Scholar
 21.Lamport, L.: Lower bounds for asynchronous consensus. In: Schiper, A., Shvartsman, A.A., Weatherspoon, H., Zhao, B.Y. (eds.) Future Directions in Distributed Computing. LNCS, vol. 2584, pp. 22–23. Springer, Heidelberg (2003). https://doi.org/10.1007/3540377956_4CrossRefGoogle Scholar
 22.Lamport, L.: Lower bounds for asynchronous consensus. Distrib. Comput. 19(2), 104–125 (2006)CrossRefGoogle Scholar
 23.Lamport, L.: Fast byzantine paxos, 17 November 2009. uS Patent 7,620,680Google Scholar
 24.Lazic, M., Konnov, I., Widder, J., Bloem, R.: Synthesis of distributed algorithms with parameterized threshold guards. In: OPODIS (2017, to appear). http://forsyte.at/wpcontent/uploads/opodis17.pdf
 25.Lewis, H.R.: Complexity results for classes of quantificational formulas. Comput. Syst. Sci. 21(3), 317–353 (1980)MathSciNetCrossRefGoogle Scholar
 26.Liffiton, M.H., Previti, A., Malik, A., MarquesSilva, J.: Fast, flexible mus enumeration. Constraints 21(2), 223–250 (2016)MathSciNetCrossRefGoogle Scholar
 27.Liu, Y.A., Stoller, S.D., Lin, B.: From clarity to efficiency for distributed algorithms. ACM Trans. Program. Lang. Syst. 39(3), 121–1241 (2017). https://doi.org/10.1145/2994595CrossRefGoogle Scholar
 28.Martin, J.P., Alvisi, L.: Fast Byzantine consensus. IEEE Trans. Dependable Secure Comput. 3(3), 202–215 (2006)CrossRefGoogle Scholar
 29.McMillan, K.L., Padon, O.: Deductive verification in decidable fragments with ivy. In: Podelski, A. (ed.) SAS 2018. LNCS, vol. 11002, pp. 43–55. Springer, Cham (2018). https://doi.org/10.1007/9783319997254_4CrossRefGoogle Scholar
 30.Padon, O., Hoenicke, J., Losa, G., Podelski, A., Sagiv, M., Shoham, S.: Reducing liveness to safety in firstorder logic. PACMPL 2(POPL), 26:1–26:33 (2018)Google Scholar
 31.Padon, O., Hoenicke, J., McMillan, K.L., Podelski, A., Sagiv, M., Shoham, S.: Temporal prophecy for proving temporal properties of infinitestate systems. In: FMCAD, pp. 1–11. IEEE (2018)Google Scholar
 32.Padon, O., Losa, G., Sagiv, M., Shoham, S.: Paxos made EPR: decidable reasoning about distributed protocols. PACMPL 1(OOPSLA), 1081–10831 (2017)Google Scholar
 33.Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. In: Krintz, C., Berger, E. (eds.) Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, 13–17 June 2016, pp. 614–630. ACM (2016)Google Scholar
 34.Piskac, R.: Decision procedures for program synthesis and verification (2011). http://infoscience.epfl.ch/record/168994
 35.Piskac, R., de Moura, L., Bjrner, N.: Deciding effectively propositional logic using DPLL and substitution sets. J. Autom. Reason. 44(4), 401–424 (2010)MathSciNetCrossRefGoogle Scholar
 36.Rahli, V., Guaspari, D., Bickford, M., Constable, R.L.: Formal specification, verification, and implementation of faulttolerant systems using eventml. ECEASST 72 (2015). https://doi.org/10.14279/tuj.eceasst.72.1013
 37.Rahli, V., Vukotic, I., Völp, M., EstevesVerissimo, P.: Velisarios: Byzantine faulttolerant protocols powered by Coq. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 619–650. Springer, Cham (2018). https://doi.org/10.1007/9783319898841_22CrossRefGoogle Scholar
 38.Sergey, I., Wilcox, J.R., Tatlock, Z.: Programming and proving with distributed protocols. PACMPL 2(POPL), 28:1–28:30 (2018)Google Scholar
 39.Song, Y.J., van Renesse, R.: Bosco: onestep Byzantine asynchronous consensus. In: Taubenfeld, G. (ed.) DISC 2008. LNCS, vol. 5218, pp. 438–450. Springer, Heidelberg (2008). https://doi.org/10.1007/9783540877790_30CrossRefGoogle Scholar
 40.Srikanth, T., Toueg, S.: Simulating authenticated broadcasts to derive simple faulttolerant algorithms. Dist. Comp. 2, 80–94 (1987)CrossRefGoogle Scholar
 41.Stoilkovska, I., Konnov, I., Widder, J., Zuleger, F.: Verifying safety of synchronous faulttolerant algorithms by bounded model checking. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 357–374. Springer, Cham (2019). https://doi.org/10.1007/9783030174651_20CrossRefGoogle Scholar
 42.Taube, M., et al.: Modularity for decidability of deductive verification with applications to distributed systems. In: PLDI, pp. 662–677. ACM (2018)CrossRefGoogle Scholar
 43.Wilcox, J.R., et al.: Verdi: a framework for implementing and formally verifying distributed systems. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, 15–17 June 2015, pp. 357–368 (2015). https://doi.org/10.1145/2737924.2737958
 44.Woos, D., Wilcox, J.R., Anton, S., Tatlock, Z., Ernst, M.D., Anderson, T.E.: Planning for change in a formal verification of the raft consensus protocol. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, 20–22 January 2016, pp. 154–165 (2016). https://doi.org/10.1145/2854065.2854081
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.