Tezla，一种用于Michelson智能合约静态分析的中间表示
Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts
摘要：
本文介绍了Tezla，这是Michelson智能合约的中间表示，可以简化静态智能合约分析器的设计。这种中间表示使用存储并保留原始智能合约的语义，ow和资源使用。这使得像气体消耗这样的属性能够被静态地验证。我们为Tezla提供了Michelson智能合约的自动化反编译器。为了支持我们关于Tezla充分性的主张，我们开发了一个静态分析器，它利用Michelson智能合约的Tezla表示来证明简单但不平凡的属性。
英文摘要：
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 preserves the semantics, ow 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
