一句话：面向逻辑式 DSL De-Con 编写的声明式智能合约，提出自动化安全验证工具 DCV，可自动推断归纳不变式。
智能合约如今管理着大量数字资产，合约中的缺陷已造成严重经济损失，因此验证合约正确性成为一项重要任务。本文提出了自动化安全验证工具 DCV，其目标是使用 De-Con 编写的声明式智能合约——De-Con 是一种基于逻辑的领域特定语言，同时用于智能合约的实现与规约。DCV 通过数学归纳法证明安全性质，并能借助启发式模式自动推断归纳不变式，无需开发者提供任何注解。作者在 23 个基准合约上进行了评估，结果表明 DCV 能够有效验证从公开代码仓库改编而来的智能合约，并且可以验证其他工具无法支持的合约；此外，DCV 在验证时间上显著优于基线工具。
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 De-Con, 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 23 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.