隨著計(jì)算機(jī)技術(shù)應(yīng)用的日益普及,軟件系統(tǒng)的規(guī)模和復(fù)雜性急劇增大,軟件在越來(lái)越多的系統(tǒng)中成為主要的組成部分。在安全攸關(guān)的應(yīng)用領(lǐng)域,軟件系統(tǒng)的可靠性至關(guān)重要,這些軟件的失效將導(dǎo)致災(zāi)難性的后果。因此,驗(yàn)證程序的正確性是非常必要的。然而,對(duì)程序的人工驗(yàn)證通常是枯燥、困難的。因此,提高程序驗(yàn)證的自動(dòng)化程度、減少人工依賴(lài)是軟件驗(yàn)證中的重要研究?jī)?nèi)容。程序中常常對(duì)復(fù)雜數(shù)據(jù)結(jié)構(gòu)進(jìn)行操作。典型的復(fù)雜數(shù)據(jù)結(jié)構(gòu)包括數(shù)組、鏈表、圖、甚至遞歸的數(shù)據(jù)結(jié)構(gòu)等。驗(yàn)證這類(lèi)程序的正確性需要分析和使用數(shù)據(jù)結(jié)構(gòu)（及其中的元素）具有的性質(zhì)。然而,自動(dòng)/半自動(dòng)地對(duì)這類(lèi)程序進(jìn)行推理和驗(yàn)證是一個(gè)很有挑戰(zhàn)的問(wèn)題:首先,它們具有復(fù)雜的語(yǔ)義;其次,程序中復(fù)雜數(shù)據(jù)結(jié)構(gòu)的大小可以非常大甚至未知,這意味著非常大數(shù)量或者未知數(shù)量的變量。本文基于數(shù)據(jù)流分析/邏輯推理等技術(shù)針對(duì)復(fù)雜數(shù)據(jù)結(jié)構(gòu)程序的分析和驗(yàn)證問(wèn)題展開(kāi)研究,在提高驗(yàn)證的自動(dòng)化程度方面取得以下結(jié)果:●提出了一種自動(dòng)化地發(fā)現(xiàn)數(shù)組程序中全稱(chēng)量詞不變式的方法。數(shù)組大小可以非常大甚至未知,因此驗(yàn)證數(shù)組程序經(jīng)常需要使用和處理全稱(chēng)量詞性質(zhì)。該方法能夠分析按照特定順序訪(fǎng)問(wèn)一維或者多維數(shù)組的程序,然后合成不變式... 

【文章來(lái)源】：南京大學(xué)江蘇省211工程院校985工程院校教育部直屬院校

【文章頁(yè)數(shù)】：156 頁(yè)

【學(xué)位級(jí)別】：博士

【文章目錄】：
摘要
Abstract
第一章 緒論
    1.1 研究背景
        1.1.1 程序驗(yàn)證
        1.1.2 程序分析
    1.2 研究問(wèn)題
    1.3 主要工作
    1.4 論文組織結(jié)構(gòu)
第二章 程序分析和驗(yàn)證的基本概念
    2.1 程序驗(yàn)證
        2.1.1 Hoare邏輯
        2.1.2 Scope邏輯
    2.2 抽象解釋
    2.3 不變式自動(dòng)生成技術(shù)
    2.4 本章小結(jié)
第三章 自動(dòng)合成數(shù)組程序的全稱(chēng)量詞不變式
    3.1 一個(gè)例子
    3.2 歸納循環(huán)程序(Induction Loop Programs)
    3.3 數(shù)組性質(zhì)
    3.4 性質(zhì)的內(nèi)存域
    3.5 預(yù)分析
    3.6 數(shù)組性質(zhì)分析
        3.6.1 數(shù)據(jù)流值
        3.6.2 join操作
        3.6.3 流函數(shù)(Flow Function)
    3.7 工具實(shí)現(xiàn)和實(shí)驗(yàn)
        3.7.1 小程序的分析結(jié)果
        3.7.2 SV-COMP數(shù)組benchmark分析結(jié)果
        3.7.3 與其他工具比較
    3.8 本章小結(jié)
第四章 自動(dòng)合成線(xiàn)性數(shù)據(jù)結(jié)構(gòu)程序量詞和析取(FOL)不變式的框架
    4.1 語(yǔ)言和預(yù)備知識(shí)
        4.1.1 擴(kuò)展歸納循環(huán)程序
        4.1.2 性質(zhì)
        4.1.3 性質(zhì)的內(nèi)存域
    4.2 框架
    4.3 預(yù)分析標(biāo)識(shí)循環(huán)控制變量
    4.4 用戶(hù)提供的不包含量詞的原子性質(zhì)分析
    4.5 lift分析
        4.5.1 量詞和析取性質(zhì)的格
        4.5.2 量詞和析取性質(zhì)集合的格
        4.5.3 D_L上的抽象解釋
    4.6 終止性(Termination)和正確性(Soundness)
        4.6.1 終止性
        4.6.2 正確性
    4.7 工具與實(shí)驗(yàn)
        4.7.1 一些例子上的分析結(jié)果
        4.7.2 SV-COMP array-examples benchmark上的分析結(jié)果以及相關(guān)工具比較
    4.8 本章小結(jié)
第五章 交互式復(fù)雜數(shù)據(jù)結(jié)構(gòu)程序分析框架
    5.1 一個(gè)例子
    5.2 背景與預(yù)備知識(shí)
        5.2.1 迭代數(shù)據(jù)流框架
        5.2.2 抽象域的組合
    5.3 交互式迭代數(shù)據(jù)流框架
        5.3.1 前向交互式迭代數(shù)據(jù)流分析方程
        5.3.2 錯(cuò)誤外部性質(zhì)的處理方法
        5.3.3 交互式數(shù)據(jù)流分析的組合
    5.4 案例研究
        5.4.1 元素屬于分析
        5.4.2 容器相交分析和容器內(nèi)互異分析
        5.4.3 案例程序上的分析結(jié)果
    5.5 本章小結(jié)
第六章 通過(guò)抽象程序證明復(fù)雜數(shù)據(jù)結(jié)構(gòu)具體程序
    6.1 一個(gè)例子
        6.1.1 利用抽象程序證明具體程序
    6.2 程序一致性關(guān)系
        6.2.1 程序語(yǔ)法
        6.2.2 精化關(guān)系
        6.2.3 一致性關(guān)系
    6.3 抽象程序和具體程序的對(duì)應(yīng)關(guān)系
        6.3.1 變量關(guān)系
        6.3.2 程序點(diǎn)關(guān)系
    6.4 驗(yàn)證義務(wù)
        6.4.1 基本驗(yàn)證義務(wù)
        6.4.2 簡(jiǎn)化證明義務(wù)
    6.5 案例研究
        6.5.1 reach程序
        6.5.2 Schorre-Waite程序
    6.6 本章小結(jié)
第七章 總結(jié)與展望
    7.1 論文的主要工作
    7.2 進(jìn)一步的工作
參考文獻(xiàn)
攻讀博士學(xué)位期間完成的學(xué)術(shù)成果
致謝



本文編號(hào)：3631446