面向形式化证明的命令生成技术

摘要：

随着软件规模的不断增大,软件安全问题日益严重.作为软件系统安全检测的有效手段,形式化证明旨在利用数学方法完成对软件属性的严格验证.常用的形式化证明方法利用模式匹配来进行定理证明,但存在策略生成不完备等缺陷.本文提出一种基于注意力机制的命令预测框架,将LSTM与Coq结合,预测定理证明过程中的策略和参数.实验结果表明本文提出的模型在生成命令的准确度方面高于现有工作(本工作预测命令准确率为28.31％).

关键词：形式化证明;Coq;命令预测;LSTM;注意力机制

所属期刊栏目：31

资助基金：国家自然科学基金61972369

在线出版日期：2022-01-21（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：273-278