Smart contracts and opportunities for formal methods

Andrew Miller, Zhicheng Cai, Somesh Jha

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Smart contracts are programs that run atop of a blockchain infrastructure. They have emerged as an important new programming model in cryptocurrencies like Ethereum, where they regulate flow of money and other digital assets according to user-defined rules. However, the most popular smart contract languages favor expressiveness rather than safety, and bugs in smart contracts have already lead to significant financial losses from accidents. Smart contracts are also appealing targets for hackers since they can be monetized. For these reasons, smart contracts are an appealing opportunity for systematic auditing and validation, and formal methods in particular. In this paper, we survey the existing smart-contract ecosystem and the existing tools for analyzing smart contracts. We then pose research challenges for formal-methods and program analysis applied to smart contracts.

Original languageEnglish (US)
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation. Industrial Practice - 8th International Symposium, ISoLA 2018, Proceedings
EditorsTiziana Margaria, Bernhard Steffen
PublisherSpringer-Verlag
Pages280-299
Number of pages20
ISBN (Print)9783030034269
DOIs
StatePublished - Jan 1 2018
Event8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018 - Limassol, Cyprus
Duration: Nov 5 2018Nov 9 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11247 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018
CountryCyprus
CityLimassol
Period11/5/1811/9/18

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Smart contracts and opportunities for formal methods'. Together they form a unique fingerprint.

  • Cite this

    Miller, A., Cai, Z., & Jha, S. (2018). Smart contracts and opportunities for formal methods. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice - 8th International Symposium, ISoLA 2018, Proceedings (pp. 280-299). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11247 LNCS). Springer-Verlag. https://doi.org/10.1007/978-3-030-03427-6_22