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
File in questo prodotto:
File Dimensione Formato  
main.pdf

Solo gestori archivio

Descrizione: Articolo principale
Tipologia: versione pre-print
Dimensione 747.14 kB
Formato Adobe PDF
  Visualizza/Apri   Richiedi una copia
747.14 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Questionario e social

Condividi su:
Impostazioni cookie