Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH scholarly article en Braithwaite, Sean; Buchman, Ethan; Konnov, Igor; Milosevic, Zarko; Stoilkovska, Ilina; Widder, Josef; Zamfir, Anca https://www.dagstuhl.de/oasics License: Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-134238
URL:

; ; ; ; ; ;

Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper)

pdf-format:


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}
}

Keywords: Blockchain, Fault Tolerance, Byzantine Faults, Model Checking
Seminar: 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)
Issue date: 2020
Date of publication: 11.12.2020
Supplementary Material: https://github.com/tendermint/spec/tree/master/rust-spec/fastsync


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI