DROPS

Document

Short Paper

DOI: 10.4230/OASIcs.FMBC.2020.8

Towards Verifying the Bitcoin-S Library (Short Paper)

Authors: Ramon Boss, Kai Brünnler, and Anna Doukmak

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

Abstract

We try to verify properties of the Bitcoin-S library, a Scala implementation of parts of the Bitcoin protocol. We use the Stainless verifier which supports programs in a fragment of Scala called Pure Scala. Since Bitcoin-S is not written in this fragment, we extract the relevant code from it and rewrite it until we arrive at code that we successfully verify. In that process we find and fix two bugs in Bitcoin-S.

Cite as

Ramon Boss, Kai Brünnler, and Anna Doukmak. Towards Verifying the Bitcoin-S Library (Short Paper). In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 8:1-8:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{boss_et_al:OASIcs.FMBC.2020.8,
  author =	{Boss, Ramon and Br\"{u}nnler, Kai and Doukmak, Anna},
  title =	{{Towards Verifying the Bitcoin-S Library}},
  booktitle =	{2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
  pages =	{8:1--8:9},
  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.8},
  URN =		{urn:nbn:de:0030-drops-134212},
  doi =		{10.4230/OASIcs.FMBC.2020.8},
  annote =	{Keywords: Bitcoin, Scala, Bitcoin-S, Stainless}
}

Search Results

Documents authored by Boss, Ramon

Towards Verifying the Bitcoin-S Library (Short Paper)

Abstract

Cite as

Thanks for your feedback!

Could not send message