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

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

Igor Konnov 1, 2 Stephan Merz 1, 2 
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
2 MOSEL - Proof-oriented development of computer-based systems
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 metadata

Cited literature [16 references]  Display  Hide  Download
Contributor : Igor Konnov Connect in order to contact the contributor
Submitted on : Friday, October 19, 2018 - 5:23:12 PM
Last modification on : Saturday, June 25, 2022 - 7:42:33 PM
Long-term archiving on: : Sunday, January 20, 2019 - 4:08:31 PM


Files produced by the author(s)


  • HAL Id : hal-01899723, version 1



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⟩



Record views


Files downloads