基于 Move Prover 的智能合约快速可靠形式化验证
编程语言
2022-02-15 v3 符号计算
软件工程
摘要
Move Prover (MVP) 是一种用于 Move 编程语言编写的智能合约的形式化验证器。MVP 具有富有表现力的规约语言，并且足够快速和可靠，开发人员可在几分钟内常规运行它，并在集成测试中执行。除了智能合约和 Move 语言的简洁性外，三种变换保证了 MVP 的实用性：(1) 无别名内存模型，(2) 细粒度不变量检查，以及 (3) 单态化。Diem 区块链的 Move 代码已被广泛规约，并且可由 MVP 在几分钟内完全验证。Diem 框架中的变更在集成到 GitHub 上的开源仓库之前必须成功通过验证。
引用
@article{arxiv.2110.08362,
title = {Fast and Reliable Formal Verification of Smart Contracts with the Move Prover},
author = {David Dill and Wolfgang Grieskamp and Junkil Park and Shaz Qadeer and Meng Xu and Emma Zhong},
journal= {arXiv preprint arXiv:2110.08362},
year = {2022}
}