论文标题
Whylson：证明您的Michelson智能合约
WhylSon: Proving your Michelson Smart Contracts in Why3
论文作者
论文摘要
本文介绍了Whylson，这是一种用米歇尔森（Michelson）编写的智能合约的演绎验证工具，这是Tezos区块链的低级语言。 Whylson接受正式指定的Michelson合同，并将其自动将其转化为Whyml编写的等效程序，WhyMl是Why3 Framework的编程和规范语言。智能合约说明被映射到其公理语义的相应的whyml浅层中，我们也在这项工作的背景下开发了。这种方法的一个主要优点是，它允许与Why3 Framework（即其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.
