Developing secure bitcoin contracts with BitML

Atzei N.;Bartoletti M.
;Lande S.;
2019-01-01

Abstract

We present a toolchain for developing and verifying smart contracts that can be executed on Bitcoin. The toolchain is based on BitML, a recent domain-specific language for smart contracts with a computationally sound embedding into Bitcoin. Our toolchain automatically verifies relevant properties of contracts, among which liquidity, ensuring that funds do not remain frozen within a contract forever. A compiler is provided to translate BitML contracts into sets of standard Bitcoin transactions: executing a contract corresponds to appending these transactions to the blockchain. We assess our toolchain through a benchmark of representative contracts.
2019
Inglese
ESEC/FSE 2019 - Proceedings of the 2019 27th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering
9781450355728
Association for Computing Machinery
1124
1128
5
WOS:000485629300109
2-s2.0-85071914633
http://dl.acm.org/citation.cfm?id=3338906
27th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2019
Contributo
Comitato scientifico
26-30 August 2019
Tallinn, Estonia
internazionale
scientifica
Bitcoin; Smart contracts; Verification
sì
4 Contributo in Atti di Convegno (Proceeding)::4.1 Contributo in Atti di convegno
Atzei, N.; Bartoletti, M.; Lande, S.; Yoshida, N.; Zunino, R.
273
5
4.1 Contributo in Atti di convegno
reserved
info:eu-repo/semantics/conferencePaper
Files in This Item:
File Size Format  
main.pdf

Solo gestori archivio

Description: Articolo principale
Type: versione pre-print
Size 747.14 kB
Format Adobe PDF
& nbsp; View / Open   Request a copy
747.14 kB Adobe PDF & nbsp; View / Open   Request a copy

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

Questionnaire and social

Share on:
Impostazioni cookie