A logic-based framework for verifying consensus algorithms Conference Paper

Author(s): Drǎgoi, Cezara; Henzinger, Thomas A; Veith, Helmut; Widder, Josef; Zufferey, Damien
Title: A logic-based framework for verifying consensus algorithms
Title Series: LNCS
Affiliation IST Austria
Abstract: Fault-tolerant distributed algorithms play an important role in ensuring the reliability of many software applications. In this paper we consider distributed algorithms whose computations are organized in rounds. To verify the correctness of such algorithms, we reason about (i) properties (such as invariants) of the state, (ii) the transitions controlled by the algorithm, and (iii) the communication graph. We introduce a logic that addresses these points, and contains set comprehensions with cardinality constraints, function symbols to describe the local states of each process, and a limited form of quantifier alternation to express the verification conditions. We show its use in automating the verification of consensus algorithms. In particular, we give a semi-decision procedure for the unsatisfiability problem of the logic and identify a decidable fragment. We successfully applied our framework to verify the correctness of a variety of consensus algorithms tolerant to both benign faults (message loss, process crashes) and value faults (message corruption).
Keywords: model checking; software reliability; Algorithms; Abstracting; Application programs; Cardinality constraints; Communication graphs; Consensus algorithms; Function symbols; Logic-based frameworks; Semi-decision procedures; Software applications; Verification condition
Conference Title: VMCAI: Verification, Model Checking and Abstract Interpretation
Volume: 8318
Conference Dates: January 20 - 21, 2014
Conference Location: San Diego, CA, USA
Publisher: Springer  
Date Published: 2014-01-01
Start Page: 161
End Page: 181
Sponsor: Supported by the National Research Network RiSE of the Austrian Science Fund (FWF) and by the Vienna Science and Technology Fund (WWTF) through grant PROSEED and by the ERC Advanced Grant QUAREM.
DOI: 10.1007/978-3-642-54013-4_10
Open access: yes (repository)
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work