License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.FMBC.2020.10
URN: urn:nbn:de:0030-drops-134238
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13423/
Braithwaite, Sean ;
Buchman, Ethan ;
Konnov, Igor ;
Milosevic, Zarko ;
Stoilkovska, Ilina ;
Widder, Josef ;
Zamfir, Anca
Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper)
Abstract
Blockchain synchronization is one of the core protocols of Tendermint blockchains. In this short paper, we discuss our recent efforts in formal specification of the protocol and its implementation, as well as some initial model checking results. We demonstrate that the protocol quality and understanding can be improved by writing specifications and model checking them.
BibTeX - Entry
@InProceedings{braithwaite_et_al:OASIcs:2020:13423,
author = {Sean Braithwaite and Ethan Buchman and Igor Konnov and Zarko Milosevic and Ilina Stoilkovska and Josef Widder and Anca Zamfir},
title = {{Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper)}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {10:1--10:8},
series = {OpenAccess Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bruno Bernardo and Diego Marmsoler},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/13423},
URN = {urn:nbn:de:0030-drops-134238},
doi = {10.4230/OASIcs.FMBC.2020.10},
annote = {Keywords: Blockchain, Fault Tolerance, Byzantine Faults, Model Checking}
}
