Skip to Main content Skip to Navigation
Conference papers

Tutorial: Parameterized Verification with Byzantine Model Checker

Abstract : Threshold guards are a basic primitive of many fault-tolerant algorithms that solve classical problems of distributed computing, such as reliable broadcast, two-phase commit, and consensus. Moreover, threshold guards can be found in recent blockchain algorithms such as Tendermint consensus. In this tutorial, we give an overview of the techniques implemented in Byzantine Model Checker (ByMC). ByMC implements several techniques for automatic verification of threshold-guarded distributed algorithms. These algorithms have the following features: (1) up to t of processes may crash or behave Byzantine; (2) the correct processes count messages and make progress when they receive sufficiently many messages, e.g., at least $$t+1$$; (3) the number n of processes in the system is a parameter, as well as t; (4) and the parameters are restricted by a resilience condition, e.g., $$n > 3t$$. Traditionally, these algorithms were implemented in distributed systems with up to ten participating processes. Nowadays, they are implemented in distributed systems that involve hundreds or thousands of processes. To make sure that these algorithms are still correct for that scale, it is imperative to verify them for all possible values of the parameters.
Complete list of metadata

https://hal.inria.fr/hal-03283235
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Friday, July 9, 2021 - 5:53:45 PM
Last modification on : Thursday, January 6, 2022 - 11:38:05 AM
Long-term archiving on: : Sunday, October 10, 2021 - 8:28:45 PM

File

 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2023-01-01

Please log in to resquest access to the document

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Igor Konnov, Marijana Lazić, Ilina Stoilkovska, Josef Widder. Tutorial: Parameterized Verification with Byzantine Model Checker. 40th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2020, Valletta, Malta. pp.189-207, ⟨10.1007/978-3-030-50086-3_11⟩. ⟨hal-03283235⟩

Share

Metrics

Record views

40