MobilityReadingGroup

π-calculus, Session Types research at Imperial College

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

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.

@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},
  pages = {--},
  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},
  pages = {--},
  year = 2019
}