<div class="csl-bib-body">
<div class="csl-entry">Konnov, I., Lazic, M., Stoilkovska, I., & Widder, J. (2020). Tutorial: Parameterized Verification with Byzantine Model Checker. In <i>Formal Techniques for Distributed Objects, Components, and Systems. 40th IFIP WG 6.1 International Conference, FORTE 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15–19, 2020, Proceedings</i> (pp. 189–207). Springer. https://doi.org/10.34726/422</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/16502
-
dc.identifier.uri
https://doi.org/10.34726/422
-
dc.description.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.
en
dc.description.sponsorship
European Research Council (ERC)
-
dc.description.sponsorship
Interchain Foundation, Switzerland
-
dc.description.sponsorship
Austrian Science Fund (FWF)
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
distributed systems
en
dc.subject
fault tolerance
en
dc.subject
parameterized model checking
en
dc.title
Tutorial: Parameterized Verification with Byzantine Model Checker
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Urheberrechtsschutz
de
dc.rights.license
In Copyright
en
dc.identifier.doi
10.34726/422
-
dc.relation.isbn
978-3-030-50086-3
-
dc.relation.doi
10.1007/978-3-030-50086-3
-
dc.description.startpage
189
-
dc.description.endpage
207
-
dc.relation.grantno
787367
-
dc.relation.grantno
W1255
-
dc.type.category
Full-Paper Contribution
-
tuw.booktitle
Formal Techniques for Distributed Objects, Components, and Systems. 40th IFIP WG 6.1 International Conference, FORTE 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15–19, 2020, Proceedings
-
tuw.container.volume
12136
-
tuw.peerreviewed
true
-
tuw.book.ispartofseries
Lecture Notes in Computer Science
-
tuw.relation.publisher
Springer
-
tuw.version
am
-
tuw.publication.invited
invited
-
tuw.publication.orgunit
E192 - Institut für Logic and Computation
-
tuw.publisher.doi
10.1007/978-3-030-50086-3_11
-
dc.description.numberOfPages
19
-
dc.rights.identifier
Urheberrechtsschutz
de
dc.rights.identifier
In Copyright
en
tuw.relation.issn
0302-9743
-
tuw.relation.eissn
1611-3349
-
item.cerifentitytype
Publications
-
item.openairetype
conference paper
-
item.languageiso639-1
en
-
item.fulltext
with Fulltext
-
item.openaccessfulltext
Open Access
-
item.grantfulltext
open
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E191-02 - Forschungsbereich Embedded Computing Systems
-
crisitem.author.dept
E191-02 - Forschungsbereich Embedded Computing Systems