汇编级顺序语句块的自动形式化规约及其验证

摘要：

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

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

所属期刊栏目：45

分类号：TP391(计算技术、计算机技术)

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

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

页数：共7页

页码：64-69,77