Search Results

Documents authored by Braithwaite, Sean


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

Authors: Sean Braithwaite, Ethan Buchman, Igor Konnov, Zarko Milosevic, Ilina Stoilkovska, Josef Widder, and Anca Zamfir

Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)


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.

Cite as

Sean Braithwaite, Ethan Buchman, Igor Konnov, Zarko Milosevic, Ilina Stoilkovska, Josef Widder, and Anca Zamfir. Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper). In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 10:1-10:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{braithwaite_et_al:OASIcs.FMBC.2020.10,
  author =	{Braithwaite, Sean and Buchman, Ethan and Konnov, Igor and Milosevic, Zarko and Stoilkovska, Ilina and Widder, Josef and Zamfir, Anca},
  title =	{{Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol}},
  booktitle =	{2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
  pages =	{10:1--10:8},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-169-6},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{84},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.10},
  URN =		{urn:nbn:de:0030-drops-134238},
  doi =		{10.4230/OASIcs.FMBC.2020.10},
  annote =	{Keywords: Blockchain, Fault Tolerance, Byzantine Faults, Model Checking}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail