用于指针逻辑的自动定理证明器的设计与实现

发布时间：2022-07-02 12:18

　　对高可信软件需求的增加使得指针程序的验证成为近十几年的研究热点,自动定理证明作为形式化方法之一,在软件验证和程序分析工具当中发挥着及其重要的作用。然而,自动定理证明本身是一个非常难于解决的问题,尤其是待解决的问题中存在着指针以及涉及到指针的递归定义的谓词的情况下。考虑到以上问题,我们在一个出具证明编译器框架中设计并实现了一个自动定理证明器和一个起辅助作用的证明检查器,来帮助完成指针程序的验证。实验结果证明,我们的实现不但具有创新性而且具有实际可行性。在本文中,我们首先介绍了项目的研究背景和理论基础,然后提出了一种为指针逻辑来设计自动定理证明器的新技术,这项技术主要是基于变换和替代,我们已经在一个被称为APL的工具中实现了该技术。指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析。此外,本文还介绍了APL自动定理证明器的详细设计和实现,描述了一些关键算法,比如指针逻辑决策过程,整型线性算术决策过程,证明检查算法等等。APL定理证明器是完全自动的,并且APL所产生的证明可以被有效的记录和检查。在出具证明编译器PLCC 2中,我们调用了APL自动定理证明器,并对一些具有代表性的程... 

【文章页数】：98 页

【学位级别】：博士

【文章目录】：
摘要
ABSTRACT
第1章 绪论
    1.1 背景研究
        1.1.1 形式化方法
        1.1.2 指针程序验证
        1.1.3 定理证明器
        1.1.4 证明检查器
        1.1.5 模型检查
    1.2 研究现状
        1.2.1 分离逻辑
        1.2.2 指针断言逻辑
        1.2.3 形状分析
        1.2.4 出具证明编译器
    1.3 问题描述
    1.4 本文概述
        1.4.1 所做研究
        1.4.2 本文贡献
        1.4.3 章节安排
第2章 指针逻辑
    2.1 基本概念
    2.2 断言语言
        2.2.1 断言语言设计
        2.2.2 断言演算
    2.3 规范语言
    2.4 公理和推理规则
第3章 APL自动定理证明器
    3.1 APL系统组成
    3.2 主函数算法
    3.3 验证条件
    3.4 验证条件检查器
    3.5 指针逻辑决策过程
        3.5.1 公理及推理规则
        3.5.2 决策过程
    3.6 整型线性算术决策过程
        3.6.1 Presburger算术
        3.6.2 相关研究
        3.6.3 Cooper算法
    3.7 生成证明
    3.8 保存证明
第4章 证明检查器
    4.1 基本原理
    4.2 证明检查算法
    4.3 对比分析
第5章 实验结果
    5.1 实验数据
    5.2 实验结果分析比较
第6章 结束语
    6.1 工作总结
    6.2 进一步工作
参考文献
附录1 验证条件的数据结构定义
附录2 Presburger算术的数据结构定义
附录3 APL的文件组成及函数功能说明
致谢
在读期间发表的学术论文与取得的研究成果


【参考文献】：
期刊论文
[1]一种用于指针程序安全性证明的指针逻辑[J]. 陈意云,华保健,葛琳,王志芳.  计算机学报. 2008(03)



本文编号：3654350