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

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

【學位級別】：博士

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


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



本文編號：3654350