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.8
URN: urn:nbn:de:0030-drops-134212
Go to the corresponding OASIcs Volume Portal

Boss, Ramon ; Br├╝nnler, Kai ; Doukmak, Anna

Towards Verifying the Bitcoin-S Library (Short Paper)

OASIcs-FMBC-2020-8.pdf (0.4 MB)


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.

BibTeX - Entry

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

Keywords: Bitcoin, Scala, Bitcoin-S, Stainless
Collection: 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)
Issue Date: 2020
Date of publication: 11.12.2020
Supplementary Material: The original Bitcoin-S code we started from, the extracted code, and the finally verified code are available in our GitHub repository:

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