Current browse context:
cs.LO
Change to browse by:
References & Citations
Computer Science > Logic in Computer Science
Title: Reactive Synthesis of Smart Contract Control Flows
(Submitted on 12 May 2022 (v1), revised 13 May 2022 (this version, v2), latest version 27 Jul 2023 (v5))
Abstract: Smart contracts are small but highly error-prone programs that implement agreements between multiple parties. We present a reactive synthesis workflow for the automatic construction of finite-state machines implementing the control flow of a smart contract. As specification language, we use temporal stream logic (TSL), which builds on LTL but adds additional mechanisms to reason about the control flow of infinite data. Our specifications not only reason about the order of transactions based on guards like access rights, but also include the updates of fields necessary for a correct control flow. We show how to comprehensively specify the control flow of various types of common smart contracts, including auctions, asset transfers, and crowd funding protocols. Our tool SCSynt implements the approach using BDD-based symbolic algorithms, resulting in a fast reactive control flow synthesis.
Submission history
From: Jana Hofmann [view email][v1] Thu, 12 May 2022 11:52:40 GMT (163kb,D)
[v2] Fri, 13 May 2022 07:14:36 GMT (163kb,D)
[v3] Sun, 21 Aug 2022 18:18:17 GMT (184kb,D)
[v4] Thu, 23 Feb 2023 18:09:23 GMT (156kb,D)
[v5] Thu, 27 Jul 2023 09:50:58 GMT (127kb,D)
Link back to: arXiv, form interface, contact.