Conference Paper/Proceeding/Abstract 244 views 20 downloads
A model of Solidity-style smart contracts in the theorem prover Agda
2023 IEEE International Conference on Artificial Intelligence, Blockchain, and Internet of Things (AIBThings), Pages: 1 - 10
Swansea University Author:
Anton Setzer
-
PDF | Accepted Manuscript
Author accepted manuscript document released under the terms of a Creative Commons CC-BY licence using the Swansea University Research Publications Policy (rights retention).
Download (251.04KB)
DOI (Published version): 10.1109/aibthings58340.2023.10292478
Abstract
The use of smart contracts is transforming traditional industry and business practices. It enables the automatic enforcement of contractual terms without the need for a trusted third party. Smart contracts can automate a variety of transactions on Blockchain. Despite their numerous benefits, some ch...
| Published in: | 2023 IEEE International Conference on Artificial Intelligence, Blockchain, and Internet of Things (AIBThings) |
|---|---|
| ISBN: | 979-8-3503-2235-4 979-8-3503-2234-7 |
| Published: |
IEEE
2023
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa64153 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
The use of smart contracts is transforming traditional industry and business practices. It enables the automatic enforcement of contractual terms without the need for a trusted third party. Smart contracts can automate a variety of transactions on Blockchain. Despite their numerous benefits, some challenges, such as security vulnerabilities, still need to be addressed before smart contracts can be widely adopted.This paper introduces two models of smart contracts – one simple and one more complex – using the interactive theorem prover Agda. This is a step towards converting the previous work of verifying Bitcoin smart contracts using weakest preconditions [1], [2] to Ethereum’s Solidity-style [3] smart contracts. Since Ethereum’s contracts are object-oriented, this model is substantially more complex than Bitcoin’s. We provide models supporting simple and complex executions, the calling of other contracts, and functions referring to addresses and messages. Furthermore, these models also support transferring money to other contracts and updating specific contracts, and the more complex model includes gas cost and pure functions. |
|---|---|
| Keywords: |
Ethereum, smart contracts, Agda proof assistant, cryptocurrency, theorem prover, Solidity, Model of soliditystyle, transaction, blockchain |
| College: |
Faculty of Science and Engineering |
| Start Page: |
1 |
| End Page: |
10 |