2026-07-21T14:19:01Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13417 2024-03-06T10:31:05Z ddc:004 open_access

Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts Santos Reis, João Crocker, Paul Melo de Sousa, Simão Intermediate representation Static analysis Tezos blockchain Michelson This paper introduces Tezla, an intermediate representation of Michelson smart contracts that eases the design of static smart contract analysers. This intermediate representation uses a store and aims to preserve the semantics, flow and resource usage of the original smart contract. This enables properties like gas consumption to be statically verified. We provide an automated decompiler of Michelson smart contracts to Tezla. In order to support our claim about the adequacy of Tezla, we develop a static analyser that takes advantage of the Tezla representation of Michelson smart contracts to prove simple but non-trivial properties. Schloss Dagstuhl – Leibniz-Zentrum für Informatik João Santos Reis and Paul Crocker and Simão Melo de Sousa 2020 Is Part Of OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.FMBC.2020.4 urn:nbn:de:0030-drops-134176 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.4 eng https://creativecommons.org/licenses/by/3.0/legalcode