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

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

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

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

【文章目錄】：
摘要
Abstract
第一章 緒論
    1.1 研究背景
        1.1.1 程序驗證
        1.1.2 程序分析
    1.2 研究問題
    1.3 主要工作
    1.4 論文組織結(jié)構(gòu)
第二章 程序分析和驗證的基本概念
    2.1 程序驗證
        2.1.1 Hoare邏輯
        2.1.2 Scope邏輯
    2.2 抽象解釋
    2.3 不變式自動生成技術(shù)
    2.4 本章小結(jié)
第三章 自動合成數(shù)組程序的全稱量詞不變式
    3.1 一個例子
    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 工具實現(xiàn)和實驗
        3.7.1 小程序的分析結(jié)果
        3.7.2 SV-COMP數(shù)組benchmark分析結(jié)果
        3.7.3 與其他工具比較
    3.8 本章小結(jié)
第四章 自動合成線性數(shù)據(jù)結(jié)構(gòu)程序量詞和析取(FOL)不變式的框架
    4.1 語言和預(yù)備知識
        4.1.1 擴展歸納循環(huán)程序
        4.1.2 性質(zhì)
        4.1.3 性質(zhì)的內(nèi)存域
    4.2 框架
    4.3 預(yù)分析標識循環(huán)控制變量
    4.4 用戶提供的不包含量詞的原子性質(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 工具與實驗
        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 一個例子
    5.2 背景與預(yù)備知識
        5.2.1 迭代數(shù)據(jù)流框架
        5.2.2 抽象域的組合
    5.3 交互式迭代數(shù)據(jù)流框架
        5.3.1 前向交互式迭代數(shù)據(jù)流分析方程
        5.3.2 錯誤外部性質(zhì)的處理方法
        5.3.3 交互式數(shù)據(jù)流分析的組合
    5.4 案例研究
        5.4.1 元素屬于分析
        5.4.2 容器相交分析和容器內(nèi)互異分析
        5.4.3 案例程序上的分析結(jié)果
    5.5 本章小結(jié)
第六章 通過抽象程序證明復(fù)雜數(shù)據(jù)結(jié)構(gòu)具體程序
    6.1 一個例子
        6.1.1 利用抽象程序證明具體程序
    6.2 程序一致性關(guān)系
        6.2.1 程序語法
        6.2.2 精化關(guān)系
        6.2.3 一致性關(guān)系
    6.3 抽象程序和具體程序的對應(yīng)關(guān)系
        6.3.1 變量關(guān)系
        6.3.2 程序點關(guān)系
    6.4 驗證義務(wù)
        6.4.1 基本驗證義務(wù)
        6.4.2 簡化證明義務(wù)
    6.5 案例研究
        6.5.1 reach程序
        6.5.2 Schorre-Waite程序
    6.6 本章小結(jié)
第七章 總結(jié)與展望
    7.1 論文的主要工作
    7.2 進一步的工作
參考文獻
攻讀博士學(xué)位期間完成的學(xué)術(shù)成果
致謝



本文編號：3631446