Model Checking of Fault-Tolerant Distributed Algorithms: from Classics towards Contemporary

Igor Konnov 1 Stephan Merz 1
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
Abstract : Fault-tolerant distributed algorithms-such as agreement, reliable broadcast, and consensus-lie at the heart of distributed systems. Although these algorithms are tiny in comparison to the rest of the system code, they are hard to design and verify. In this short research statement, we discuss the Byzantine model checker, which was developed for automatic verification of asynchronous fault-tolerant distributed algorithms. Further, we discuss the challenges that are posed by contemporary protocols for Blockchain consensus.
Liste complète des métadonnées

https://hal.inria.fr/hal-01899723
Contributor : Igor Konnov <>
Submitted on : Friday, October 19, 2018 - 5:23:12 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:04 PM
Document(s) archivé(s) le : Sunday, January 20, 2019 - 4:08:31 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01899723, version 1

Collections

Citation

Igor Konnov, Stephan Merz. Model Checking of Fault-Tolerant Distributed Algorithms: from Classics towards Contemporary. BCRB 2018 - DSN Workshop on Byzantine Consensus and Resilient Blockchains, Jun 2018, Luxembourg, Luxembourg. ⟨hal-01899723⟩

Share

Metrics

Record views

67

Files downloads

101