A survey of smart contract formal specification and verification
A smart contract is a computer program that allows users to automate their actions on the blockchain platform. Given the significance of smart contracts in supporting important activities across industry sectors including supply chain, finance, legal, and medical services, there is a strong demand f...
| Main Authors: | , , , , |
|---|---|
| Other Authors: | |
| Format: | Journal Article |
| Language: | English |
| Published: |
2022
|
| Subjects: | |
| Online Access: | https://hdl.handle.net/10356/160319 |
| _version_ | 1811696940420694016 |
|---|---|
| author | Tolmach, Palina Li, Yi Lin, Shang-Wei Liu, Yang Li, Zengxiang |
| author2 | School of Computer Science and Engineering |
| author_facet | School of Computer Science and Engineering Tolmach, Palina Li, Yi Lin, Shang-Wei Liu, Yang Li, Zengxiang |
| author_sort | Tolmach, Palina |
| collection | NTU |
| description | A smart contract is a computer program that allows users to automate their actions on the blockchain platform. Given the significance of smart contracts in supporting important activities across industry sectors including supply chain, finance, legal, and medical services, there is a strong demand for verification and validation techniques. Yet, the vast majority of smart contracts lack any kind of formal specification, which is essential for establishing their correctness. In this survey, we investigate formal models and specifications of smart contracts presented in the literature and present a systematic overview to understand the common trends. We also discuss the current approaches used in verifying such property specifications and identify gaps with the hope to recognize promising directions for future work. |
| first_indexed | 2024-10-01T07:47:21Z |
| format | Journal Article |
| id | ntu-10356/160319 |
| institution | Nanyang Technological University |
| language | English |
| last_indexed | 2024-10-01T07:47:21Z |
| publishDate | 2022 |
| record_format | dspace |
| spelling | ntu-10356/1603192022-07-19T05:13:59Z A survey of smart contract formal specification and verification Tolmach, Palina Li, Yi Lin, Shang-Wei Liu, Yang Li, Zengxiang School of Computer Science and Engineering Institute of High Performance Computing (A*STAR) Engineering::Computer science and engineering Smart Contract Formal Verification A smart contract is a computer program that allows users to automate their actions on the blockchain platform. Given the significance of smart contracts in supporting important activities across industry sectors including supply chain, finance, legal, and medical services, there is a strong demand for verification and validation techniques. Yet, the vast majority of smart contracts lack any kind of formal specification, which is essential for establishing their correctness. In this survey, we investigate formal models and specifications of smart contracts presented in the literature and present a systematic overview to understand the common trends. We also discuss the current approaches used in verifying such property specifications and identify gaps with the hope to recognize promising directions for future work. Energy Market Authority (EMA) Ministry of Education (MOE) National Research Foundation (NRF) This research is partially supported by the Ministry of Education, Singapore, under its Academic Research Fund Tier 1 (Award No. 2018-T1-002-069) and Tier 2 (Award No. MOE2018-T2-1-068), and by the National Research Foundation, Singapore, and the Energy Market Authority, under its Energy Programme (EP Award No. NRF2017EWT-EP003-023). 2022-07-19T05:13:59Z 2022-07-19T05:13:59Z 2022 Journal Article Tolmach, P., Li, Y., Lin, S., Liu, Y. & Li, Z. (2022). A survey of smart contract formal specification and verification. ACM Computing Surveys, 54(7), 1-38. https://dx.doi.org/10.1145/3464421 0360-0300 https://hdl.handle.net/10356/160319 10.1145/3464421 2-s2.0-85114205074 7 54 1 38 en 2018-T1-002-069 MOE2018-T2-1-068 NRF2017EWT-EP003-023 ACM Computing Surveys © 2021 Association for Computing Machinery. All rights reserved. |
| spellingShingle | Engineering::Computer science and engineering Smart Contract Formal Verification Tolmach, Palina Li, Yi Lin, Shang-Wei Liu, Yang Li, Zengxiang A survey of smart contract formal specification and verification |
| title | A survey of smart contract formal specification and verification |
| title_full | A survey of smart contract formal specification and verification |
| title_fullStr | A survey of smart contract formal specification and verification |
| title_full_unstemmed | A survey of smart contract formal specification and verification |
| title_short | A survey of smart contract formal specification and verification |
| title_sort | survey of smart contract formal specification and verification |
| topic | Engineering::Computer science and engineering Smart Contract Formal Verification |
| url | https://hdl.handle.net/10356/160319 |
| work_keys_str_mv | AT tolmachpalina asurveyofsmartcontractformalspecificationandverification AT liyi asurveyofsmartcontractformalspecificationandverification AT linshangwei asurveyofsmartcontractformalspecificationandverification AT liuyang asurveyofsmartcontractformalspecificationandverification AT lizengxiang asurveyofsmartcontractformalspecificationandverification AT tolmachpalina surveyofsmartcontractformalspecificationandverification AT liyi surveyofsmartcontractformalspecificationandverification AT linshangwei surveyofsmartcontractformalspecificationandverification AT liuyang surveyofsmartcontractformalspecificationandverification AT lizengxiang surveyofsmartcontractformalspecificationandverification |