Lamela Seijas, Pablo and Smith, David and Thompson, Simon (2020) Efficient Static Analysis of Marlowe Contracts. In: Margaria, Tiziana and Steffen, Bernhard, eds. ISoLA 2020: Leveraging Applications of Formal Methods, Verification and Validation: Applications. Lecture Notes in Computer Science . Springer, Cham, Switzerland, pp. 161-177. ISBN 978-3-030-61466-9. E-ISBN 978-3-030-61467-6. (doi:10.1007/978-3-030-61467-6_11) (KAR id:83710)
PDF
Author's Accepted Manuscript
Language: English |
|
Download this file (PDF/423kB) |
|
Request a format suitable for use with assistive technology e.g. a screenreader | |
Official URL: https://doi.org/10.1007/978-3-030-61467-6_11 |
Abstract
SMT solvers can verify properties automatically and efficiently, and they offer increasing
flexibility on the ways those properties can be described. But it is hard to predict how those ways of describing the properties affect the computational cost of verifying them.
In this paper, we discuss what we learned while implementing and optimising the static analysis for Marlowe, a domain specific language for self-enforcing financial smart-contracts that can be deployed on a blockchain.
Item Type: | Book section |
---|---|
DOI/Identification number: | 10.1007/978-3-030-61467-6_11 |
Uncontrolled keywords: | Marlowe, SMT, Cardano, blockchain, Z3, optimisation, analysis,Marlowe Playground |
Subjects: | Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, > QA76.76 Computer software |
Divisions: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
Depositing User: | S. Thompson |
Date Deposited: | 26 Oct 2020 08:47 UTC |
Last Modified: | 05 Nov 2024 12:49 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/83710 (The current URI for this page, for reference purposes) |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):