Fast and Reliable Formal Verification of Smart Contracts with the Move Prover

简介

Move Prover（MVP）是一个用于验证使用Move编程语言编写的智能合约的形式验证器。MVP具有表达能力强的规范语言，足够快速和可靠，可以在几分钟内由开发人员和集成测试例行运行。除了智能合约和Move语言的简单性外，三个转换负责MVP的实用性：（1）无别名的内存模型，（2）细粒度的不变量检查，（3）单态化。 Diem区块链的整个Move代码已经被广泛规定，并且可以在几分钟内由MVP完全验证。在Diem框架中进行更改必须经过成功验证，然后才能集成到GitHub上的开源存储库中。
作者讲解

目前尚无作者解读视频，你可点击下方【许愿开讲】按钮，许愿作者开讲~
图表
解决问题

MVP论文旨在为使用Move编程语言编写的智能合约提供一种形式验证器，以验证其正确性。
关键思路

MVP使用三种转换来提高实用性：无别名内存模型、精细的不变式检查和单态化。
其它亮点

MVP具有表达力强的规范语言，可以在几分钟内由开发人员和集成测试例程运行，Diem区块链的所有Move代码都可以在几分钟内完全验证。论文提出的方法在实践中具有较高的速度和可靠性。
相关研究

与此相关的研究包括基于其他编程语言的智能合约验证方法，如Solidity和Vyper。