面向形式化证明的命令生成技术
Command Generation Technology for Formal Proof作者机构：中国科学技术大学网络空间安全学院合肥230027 中国科学技术大学计算机科学与技术学院合肥230027
出 版 物：《计算机系统应用》 (Computer Systems & Applications)
年 卷 期：2022年第31卷第1期
页 面：273-278页
学科分类：08[工学] 081201[工学-计算机系统结构] 0812[工学-计算机科学与技术（可授工学、理学学位）] 081202[工学-计算机软件与理论]
摘 要：随着软件规模的不断增大,软件安全问题日益严重.作为软件系统安全检测的有效手段,形式化证明旨在利用数学方法完成对软件属性的严格验证.常用的形式化证明方法利用模式匹配来进行定理证明,但存在策略生成不完备等缺陷.本文提出一种基于注意力机制的命令预测框架,将LSTM与Coq结合,预测定理证明过程中的策略和参数.实验结果表明本文提出的模型在生成命令的准确度方面高于现有工作(本工作预测命令准确率为28.31%).
维普期刊数据库
同方期刊数据库