2026-07-23T18:19:10Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20852 2024-09-12T05:48:33Z ddc:004 open_access

A Dynamic Logic for Symbolic Execution for the Smart Contract Programming Language Michelson Arvay, Barnabas Doan, Thi Thu Ha Thiemann, Peter Smart Contract Blockchain Formal Verification Symbolic Execution Verification of smart contracts is an important topic in the context of blockchain technology. We study an approach to verification that is based on symbolic execution. As a formal basis for symbolic execution, we design a dynamic logic for Michelson, the smart contract language of the Tezos blockchain, and prove its soundness in the proof assistant Agda. Towards the soundness proof we formalize the concrete semantics as well as its symbolic counterpart in a unified setting. The logic encompasses single contract runs as well as inter-contract runs chained in a single transaction. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Barnabas Arvay and Thi Thu Ha Doan and Peter Thiemann 2024 Is Part Of LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2024.3 urn:nbn:de:0030-drops-208529 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.3 eng https://creativecommons.org/licenses/by/4.0/legalcode