以太坊智能合约定理证明中的形式化规约研究综述
Survey of Formal Specification Methods in Theorem Proving of Ethereum Smart Contract作者机构：南京大学计算机科学与技术系南京210023
出 版 物：《信息网络安全》 (Netinfo Security)
年 卷 期：2022年第5期
页 面：11-20页
学科分类：08[工学] 081201[工学-计算机系统结构] 0812[工学-计算机科学与技术（可授工学、理学学位）]
基 金：江苏省前沿引领技术基础研究专项[BK20202001]。
摘 要：以太坊智能合约的形式化验证是目前的研究热点,在各种形式化验证方法中,定理证明方法具有误报少、可以处理大状态空间等优点。定理证明需要强大的形式化规约表达能力作为基础。文章对现有以太坊智能合约的定理证明研究中使用的形式化规约表达方法进行综述,从智能合约开发语言和区块链内生语义的建模、智能合约安全属性和功能属性的形式化规约表达、自动定理证明和交互式定理证明的选择等角度对形式化规约方法进行比较和讨论,并指出目前的困难和未来的研究方向。
维普期刊数据库
同方期刊数据库