MobilityReadingGroup

π-calculus, Session Types research at the University of Oxford

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
}