Smart contracts manage a large number of digital assets nowadays. Bugs in these contracts have led to significant financial loss. Verifying the correctness of smart contracts is, therefore, an important task. This paper presents an automated safety verification tool, DCV, that targets declarative smart contracts written in DeCon, a logic-based domain-specific language for smart contract implementation and specification. DCV proves safety properties by mathematical induction and can automatically infer inductive invariants using heuristic patterns, without annotations from the developer. Our evaluation on 20 benchmark contracts shows that DCV is effective in verifying smart contracts adapted from public repositories, and can verify contracts not supported by other tools. Furthermore, DCV significantly outperforms baseline tools in verification time.

翻译：智能合约如今管理着大量数字资产。这些合约中的漏洞已导致重大财务损失。因此，验证智能合约的正确性是一项重要任务。本文介绍了一种自动化安全验证工具DCV，该工具针对用DeCon编写的声明式智能合约——DeCon是一种基于逻辑的领域特定语言，用于智能合约的实现与规范。DCV通过数学归纳法证明安全性性质，并能利用启发式模式自动推断归纳不变量，无需开发者提供注释。我们在20个基准合约上的评估表明，DCV能够有效验证源自公共仓库的智能合约，并且可以验证其他工具不支持合约。此外，DCV在验证时间上显著优于基线工具。