计算机工程

作者：祁龙云, 吕小亮, 路红, 黄皓

单位：1. 南京南瑞信息通信科技有限公司, 南京 210003;2. 南京大学 计算机软件新技术国家重点实验室, 南京 210023

关键词：自动形式化规约,自动化验证,定理证明器,交互式定理,形式化验证

基金：国家电网公司2018年总部科技项目"可信嵌入式操作系统关键技术研究"（SGJSNT00FZJS1800129）。

软件的形式化验证是保障软件可证明性、可靠性和安全性的重要手段，但传统形式化验证脚本的生成过程复杂且需要形式化验证专家的大量手工验证。为提高证明效率，构建一种自动证明模型，并在此基础上提出语义自动规约算法以及对所规约的语义自动生成证明脚本的算法。利用C++和Python并通过交互式定理证明器Isabelle 2017在基准数据中随机选择10个程序进行测试，结果表明，与完全人工操作相比，该算法具有较高的验证效率，可实现顺序语句块的自动化规约与验证。

来源：2019年第10期

《计算机工程》期刊编辑部

查看计算机工程杂志2019年第10期