Verification of threshold-based distributed algorithms by decomposition to decidable logics

DOI10.1007/978-3-030-25543-5_15MaRDI QIDQ6154883FDO

Authors Idan Berkovits, Marijana Lazić, Giuliano Losa, Oded Padon, Sharon Shoham

Publication date 16 February 2024

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1905.07805

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Distributed algorithms (68W15) Logic in computer science (03B70) Distributed systems (68M14)

Abstract: Verification of fault-tolerant 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 threshold-based protocols is extremely challenging as it involves two kinds of reasoning: first-order 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 one-step consensus, hybrid reliable broadcast and fast Byzantine Paxos.

Recommendations

• Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
• A logic-based framework for verifying consensus algorithms
• Complexity of Verification and Synthesis of Threshold Automata
• Eliminating message counters in synchronous threshold automata
• SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms

Cited in

(4)

• Stratified guarded first-order transition systems
• Inferring invariants with quantifier alternations: taming the search space explosion
• Symbolic model checking for TLA+ made faster
• Efficient automated reasoning about sets and multisets with cardinality constraints

This page was built for publication: Verification of threshold-based distributed algorithms by decomposition to decidable logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6154883)