Skip to Main content Skip to Navigation
Documents associated with scientific events

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
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download

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

92

Files downloads

169