Skip to main content
Kent Academic Repository

Efficient Static Analysis of Marlowe Contracts

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)


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: 08 Dec 2022 22:14 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.