复杂数据结构程序的分析和验证技术研究

发布时间：2022-02-18 19:51

　　随着计算机技术应用的日益普及,软件系统的规模和复杂性急剧增大,软件在越来越多的系统中成为主要的组成部分。在安全攸关的应用领域,软件系统的可靠性至关重要,这些软件的失效将导致灾难性的后果。因此,验证程序的正确性是非常必要的。然而,对程序的人工验证通常是枯燥、困难的。因此,提高程序验证的自动化程度、减少人工依赖是软件验证中的重要研究内容。程序中常常对复杂数据结构进行操作。典型的复杂数据结构包括数组、链表、图、甚至递归的数据结构等。验证这类程序的正确性需要分析和使用数据结构（及其中的元素）具有的性质。然而,自动/半自动地对这类程序进行推理和验证是一个很有挑战的问题:首先,它们具有复杂的语义;其次,程序中复杂数据结构的大小可以非常大甚至未知,这意味着非常大数量或者未知数量的变量。本文基于数据流分析/逻辑推理等技术针对复杂数据结构程序的分析和验证问题展开研究,在提高验证的自动化程度方面取得以下结果:●提出了一种自动化地发现数组程序中全称量词不变式的方法。数组大小可以非常大甚至未知,因此验证数组程序经常需要使用和处理全称量词性质。该方法能够分析按照特定顺序访问一维或者多维数组的程序,然后合成不变式... 

【文章来源】：南京大学江苏省211工程院校985工程院校教育部直属院校

【文章页数】：156 页

【学位级别】：博士

【文章目录】：
摘要
Abstract
第一章 绪论
    1.1 研究背景
        1.1.1 程序验证
        1.1.2 程序分析
    1.2 研究问题
    1.3 主要工作
    1.4 论文组织结构
第二章 程序分析和验证的基本概念
    2.1 程序验证
        2.1.1 Hoare逻辑
        2.1.2 Scope逻辑
    2.2 抽象解释
    2.3 不变式自动生成技术
    2.4 本章小结
第三章 自动合成数组程序的全称量词不变式
    3.1 一个例子
    3.2 归纳循环程序(Induction Loop Programs)
    3.3 数组性质
    3.4 性质的内存域
    3.5 预分析
    3.6 数组性质分析
        3.6.1 数据流值
        3.6.2 join操作
        3.6.3 流函数(Flow Function)
    3.7 工具实现和实验
        3.7.1 小程序的分析结果
        3.7.2 SV-COMP数组benchmark分析结果
        3.7.3 与其他工具比较
    3.8 本章小结
第四章 自动合成线性数据结构程序量词和析取(FOL)不变式的框架
    4.1 语言和预备知识
        4.1.1 扩展归纳循环程序
        4.1.2 性质
        4.1.3 性质的内存域
    4.2 框架
    4.3 预分析标识循环控制变量
    4.4 用户提供的不包含量词的原子性质分析
    4.5 lift分析
        4.5.1 量词和析取性质的格
        4.5.2 量词和析取性质集合的格
        4.5.3 D_L上的抽象解释
    4.6 终止性(Termination)和正确性(Soundness)
        4.6.1 终止性
        4.6.2 正确性
    4.7 工具与实验
        4.7.1 一些例子上的分析结果
        4.7.2 SV-COMP array-examples benchmark上的分析结果以及相关工具比较
    4.8 本章小结
第五章 交互式复杂数据结构程序分析框架
    5.1 一个例子
    5.2 背景与预备知识
        5.2.1 迭代数据流框架
        5.2.2 抽象域的组合
    5.3 交互式迭代数据流框架
        5.3.1 前向交互式迭代数据流分析方程
        5.3.2 错误外部性质的处理方法
        5.3.3 交互式数据流分析的组合
    5.4 案例研究
        5.4.1 元素属于分析
        5.4.2 容器相交分析和容器内互异分析
        5.4.3 案例程序上的分析结果
    5.5 本章小结
第六章 通过抽象程序证明复杂数据结构具体程序
    6.1 一个例子
        6.1.1 利用抽象程序证明具体程序
    6.2 程序一致性关系
        6.2.1 程序语法
        6.2.2 精化关系
        6.2.3 一致性关系
    6.3 抽象程序和具体程序的对应关系
        6.3.1 变量关系
        6.3.2 程序点关系
    6.4 验证义务
        6.4.1 基本验证义务
        6.4.2 简化证明义务
    6.5 案例研究
        6.5.1 reach程序
        6.5.2 Schorre-Waite程序
    6.6 本章小结
第七章 总结与展望
    7.1 论文的主要工作
    7.2 进一步的工作
参考文献
攻读博士学位期间完成的学术成果
致谢



本文编号：3631446