典型文献
以太坊智能合约定理证明中的形式化规约研究综述
文献摘要：
以太坊智能合约的形式化验证是目前的研究热点,在各种形式化验证方法中,定理证明方法具有误报少、可以处理大状态空间等优点.定理证明需要强大的形式化规约表达能力作为基础.文章对现有以太坊智能合约的定理证明研究中使用的形式化规约表达方法进行综述,从智能合约开发语言和区块链内生语义的建模、智能合约安全属性和功能属性的形式化规约表达、自动定理证明和交互式定理证明的选择等角度对形式化规约方法进行比较和讨论,并指出目前的困难和未来的研究方向.
文献关键词：
以太坊;智能合约;形式化规约;形式化验证;定理证明
中图分类号：
作者姓名：
华景煜;黄达明
作者机构：
南京大学计算机科学与技术系,南京 210023
文献出处：
引用格式：
[1]华景煜;黄达明-.以太坊智能合约定理证明中的形式化规约研究综述)[J].信息网络安全,2022(05):11-20
A类：
形式化规约
B类：
以太坊,智能合约,约定,定理证明,形式化验证,验证方法,证明方法,有误,误报,状态空间,表达能力,表达方法,全属,功能属性,交互式
AB值：
0.189375
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
