對(duì)高可信軟件需求的增加使得指針程序的驗(yàn)證成為近十幾年的研究熱點(diǎn),自動(dòng)定理證明作為形式化方法之一,在軟件驗(yàn)證和程序分析工具當(dāng)中發(fā)揮著及其重要的作用。然而,自動(dòng)定理證明本身是一個(gè)非常難于解決的問(wèn)題,尤其是待解決的問(wèn)題中存在著指針以及涉及到指針的遞歸定義的謂詞的情況下�？紤]到以上問(wèn)題,我們?cè)谝粋�(gè)出具證明編譯器框架中設(shè)計(jì)并實(shí)現(xiàn)了一個(gè)自動(dòng)定理證明器和一個(gè)起輔助作用的證明檢查器,來(lái)幫助完成指針程序的驗(yàn)證。實(shí)驗(yàn)結(jié)果證明,我們的實(shí)現(xiàn)不但具有創(chuàng)新性而且具有實(shí)際可行性。在本文中,我們首先介紹了項(xiàng)目的研究背景和理論基礎(chǔ),然后提出了一種為指針邏輯來(lái)設(shè)計(jì)自動(dòng)定理證明器的新技術(shù),這項(xiàng)技術(shù)主要是基于變換和替代,我們已經(jīng)在一個(gè)被稱(chēng)為APL的工具中實(shí)現(xiàn)了該技術(shù)。指針邏輯作為Hoare邏輯的擴(kuò)展,可以對(duì)指針程序進(jìn)行精確的分析。此外,本文還介紹了APL自動(dòng)定理證明器的詳細(xì)設(shè)計(jì)和實(shí)現(xiàn),描述了一些關(guān)鍵算法,比如指針邏輯決策過(guò)程,整型線(xiàn)性算術(shù)決策過(guò)程,證明檢查算法等等。APL定理證明器是完全自動(dòng)的,并且APL所產(chǎn)生的證明可以被有效的記錄和檢查。在出具證明編譯器PLCC 2中,我們調(diào)用了APL自動(dòng)定理證明器,并對(duì)一些具有代表性的程... 

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

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

【文章目錄】：
摘要
ABSTRACT
第1章 緒論
    1.1 背景研究
        1.1.1 形式化方法
        1.1.2 指針程序驗(yàn)證
        1.1.3 定理證明器
        1.1.4 證明檢查器
        1.1.5 模型檢查
    1.2 研究現(xiàn)狀
        1.2.1 分離邏輯
        1.2.2 指針斷言邏輯
        1.2.3 形狀分析
        1.2.4 出具證明編譯器
    1.3 問(wèn)題描述
    1.4 本文概述
        1.4.1 所做研究
        1.4.2 本文貢獻(xiàn)
        1.4.3 章節(jié)安排
第2章 指針邏輯
    2.1 基本概念
    2.2 斷言語(yǔ)言
        2.2.1 斷言語(yǔ)言設(shè)計(jì)
        2.2.2 斷言演算
    2.3 規(guī)范語(yǔ)言
    2.4 公理和推理規(guī)則
第3章 APL自動(dòng)定理證明器
    3.1 APL系統(tǒng)組成
    3.2 主函數(shù)算法
    3.3 驗(yàn)證條件
    3.4 驗(yàn)證條件檢查器
    3.5 指針邏輯決策過(guò)程
        3.5.1 公理及推理規(guī)則
        3.5.2 決策過(guò)程
    3.6 整型線(xiàn)性算術(shù)決策過(guò)程
        3.6.1 Presburger算術(shù)
        3.6.2 相關(guān)研究
        3.6.3 Cooper算法
    3.7 生成證明
    3.8 保存證明
第4章 證明檢查器
    4.1 基本原理
    4.2 證明檢查算法
    4.3 對(duì)比分析
第5章 實(shí)驗(yàn)結(jié)果
    5.1 實(shí)驗(yàn)數(shù)據(jù)
    5.2 實(shí)驗(yàn)結(jié)果分析比較
第6章 結(jié)束語(yǔ)
    6.1 工作總結(jié)
    6.2 進(jìn)一步工作
參考文獻(xiàn)
附錄1 驗(yàn)證條件的數(shù)據(jù)結(jié)構(gòu)定義
附錄2 Presburger算術(shù)的數(shù)據(jù)結(jié)構(gòu)定義
附錄3 APL的文件組成及函數(shù)功能說(shuō)明
致謝
在讀期間發(fā)表的學(xué)術(shù)論文與取得的研究成果


【參考文獻(xiàn)】：
期刊論文
[1]一種用于指針程序安全性證明的指針邏輯[J]. 陳意云,華保健,葛琳,王志芳.  計(jì)算機(jī)學(xué)報(bào). 2008(03)



本文編號(hào)：3654350