面向形式化证明的命令生成技术
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

国家自然科学基金(61972369)


Command Generation Technology for Formal Proof
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 增强出版
  • |
  • 文章评论
    摘要:

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

    Abstract:

    With the continuous increase in software scale, software security faces increasingly severe challenges. As an effective means of detecting software system security, formal proof aims to use mathematical methods to complete rigorous verification of software attributes. Commonly used formal proof methods prove theorems with pattern matching, which, however, suffer from defects such as incomplete strategy generation. This study proposes a command prediction framework based on the attention mechanism. It combines long short-term memory (LSTM) with Coq to predict the strategies and parameters during theorem proving. The experimental results show that the model proposed in this study is superior to existing ones in the accuracy of command generation (the accuracy of command prediction is 28.31% in this paper).

    参考文献
    相似文献
    引证文献
引用本文

莫广帅,熊焰,黄文超.面向形式化证明的命令生成技术.计算机系统应用,2022,31(1):273-278

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2021-03-23
  • 最后修改日期:2021-04-19
  • 录用日期:
  • 在线发布日期: 2021-12-17
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京海淀区中关村南四街4号 中科院软件园区 7号楼305房间,邮政编码:100190
电话:010-62661041 传真: Email:csa (a) iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号