No Cover Image

Conference Paper/Proceeding/Abstract 228 views 18 downloads

A model of Solidity-style smart contracts in the theorem prover Agda

Fahad Alhabardi, Anton Setzer Orcid Logo

2023 IEEE International Conference on Artificial Intelligence, Blockchain, and Internet of Things (AIBThings), Pages: 1 - 10

Swansea University Author: Anton Setzer Orcid Logo

  • 64153.pdf

    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...

Full description

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