WhylSon：在Why3中验证您的迈克尔逊智能合约
WhylSon: Proving your Michelson Smart Contracts in Why3
摘要：
本文介绍了WhylSon，一个用Michelson编写的智能合约演绎验证工具，这是Tezos区块链的低级语言。WhylSon接受正式指定的Michelson契约，并自动将其转换为用WhyML（Why3框架的编程和规约语言）编写的等效程序。智能合约指令被映射到其公理语义的相应WhyML浅嵌入中，我们也在这项工作的上下文中开发了这一点。这种方法的一个主要优点是，它允许与Why3框架进行开箱即用的集成，即其VCGen和对几个自动定理证明器的后端支持。我们还讨论了使用WhylSon来自动证明各种注释智能合约的正确性。
英文摘要：
This paper introduces WhylSon, a deductive verification tool for smart contracts written in Michelson, which is the low-level language of the Tezos blockchain. WhylSon accepts a formally specified Michelson contract and automatically translates it to an equivalent program written in WhyML, the programming and specification language of the Why3 framework. Smart contract instructions are mapped into a corresponding WhyML shallow-embedding of the their axiomatic semantics, which we also developed in the context of this work. One major advantage of this approach is that it allows an out-of-the-box integration with the Why3 framework, namely its VCGen and the backend support for several automated theorem provers. We also discuss the use of WhylSon to automatically prove the correctness of diverse annotated smart contracts.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
