《基於反例壓縮的自動程式修正方法研究》是依託中國人民解放軍國防科技大學，由沈勝宇擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：基於反例壓縮的自動程式修正方法研究
- 項目類別：青年科學基金項目
- 項目負責人：沈勝宇
- 依託單位：中國人民解放軍國防科技大學
- 批准號：60603088
- 申請代碼：F0209
- 負責人職稱：副研究員
- 研究期限：2007-01-01 至 2009-12-31
- 支持經費：27（萬元）
中文摘要
在VLSI驗證領域，利用計算機自動修正錯誤程式，正在成為新的研究熱點。現有方法存在運算複雜性高、可解範圍小和修正結果難以理解的問題。本項目的目標在於提出全新的程式修正理論框架，以降低算法複雜性、擴大可解範圍並提高結果的可讀性。為達到上述目標，本項目將從以下方面開展研究：基於反例壓縮和程式切片方法，剔除程式中的無關變數和語句，以縮小搜尋空間，並最終降低運算複雜性；基於表達式錯誤模型、語義DELTA假設和限界互斥原理，提出程式修正博弈問題的構造、化簡和求解算法，以擴展可解範圍；依據語法DELTA假設，構造具有高度可讀性的修正表達式，以利於程式設計師理解修正結果。.本項目提出的理論框架和實現技術，能有效降低自動程式修正算法的運算複雜性、擴展其可解範圍並提高結果的可讀性。其研究成果能夠極大的提高VLSI系統設計與驗證效率，具有重大的學術價值和套用前景。
