MobilityReadingGroup

π-calculus, Session Types research at Imperial College

Developing secure Bitcoin contracts with BitML.
Nicola ATZEI, Massimo BARTOLETTI, Stefano LANDE, Nobuko YOSHIDA, Roberto ZUNINO
The ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2019). p. 1124 - 1128

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.

Paper Electronic version via DOI website bitml-lang 
@inproceedings{ABLYZ2019,
  author = {Nicola Atzei and Massimo Bartoletti and Stefano Lande and Nobuko Yoshida and Roberto Zunino},
  title = {{Developing secure Bitcoin contracts with BitML.}},
  booktitle = {The ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering},
  series = {ESEC/FSE 2019},
  pages = {1124--1128},
  publisher = {ACM},
  year = 2019
}

@inproceedings{ABLYZ2019,
  author = {Nicola Atzei and Massimo Bartoletti and Stefano Lande and Nobuko Yoshida and Roberto Zunino},
  title = {{Developing secure Bitcoin contracts with BitML.}},
  booktitle = {The ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering},
  series = {ESEC/FSE 2019},
  pages = {1124--1128},
  publisher = {ACM},
  doi = "10.1145/3338906.3341173",
  year = 2019
}