@inproceedings{d6395b49b69f4586843c13287665a840,
title = "Verifying Correctness of Smart Contracts with Conditionals",
abstract = "In this paper, we specify and verify the correctness of programs written in Bitcoin's smart contract SCRIPT in the interactive theorem prover Agda. As in the previous article [1], we use weakest preconditions of Hoare logic to specify the security property of access control, and show how to develop human-readable specifications. In this article, we include conditionals into the language. For the operational semantics we use an additional stack, the ifstack, to deal with nested conditionals. This avoids the addition of extra jump instructions, which are usually used for the operational semantics of conditionals in Forth-style stack languages. The ifstack preserves the original nesting of conditionals, and we determine an ifthenselse-theorem which allows to derive verification conditions of conditionals by referring to conditions for the if-and else-case.",
keywords = "access control, Agda, Bitcoin, Bitcoin script, blockchain control flow, cryptocurrency, Hoare logic, operational semantics, security, smart contracts, weakest precondition",
author = "Fahad Alhabardi and Bogdan Lazar and Anton Setzer",
year = "2022",
month = nov,
day = "11",
doi = "10.1109/iGETblockchain56591.2022.10087054",
language = "English",
isbn = "9781665452601",
series = "2022 IEEE 1st Global Emerging Technology Blockchain Forum: Blockchain and Beyond, iGETblockchain 2022",
publisher = "IEEE",
booktitle = "2022 IEEE 1st Global Emerging Technology Blockchain Forum",
address = "USA United States",
note = "1st IEEE Global Emerging Technology Blockchain Forum: Blockchain and Beyond, iGETblockchain 2022 ; Conference date: 07-11-2022 Through 11-11-2022",
}