《組契約束求解過程及其在程式驗證中的套用》是依託華東師範大學，由徐鳴擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：組契約束求解過程及其在程式驗證中的套用
- 項目類別：青年科學基金項目
- 項目負責人：徐鳴
- 依託單位：華東師範大學
項目摘要,結題摘要,
項目摘要
現今信息技術已經滲透到日常生活的方方面面。如何提高信息計算系統的可靠性是一個不可迴避的問題。為了追求絕對正確性這一目標，相關的驗證與檢測技術離不開各種判定過程、約束求解的理論方法。而傳統的驗證技術運用單一的約束求解算法進行推理，從一定程度上束縛了驗證技術的套用範圍。在安全攸關係統迅猛發展的時代背景下，本項目擬重點研究多種判定過程、約束求解算法和它們之間的組合問題，擴大可解約束的範圍；成果也將同時套用於計算機軟體程式的驗證問題中，為可信軟體提供紮實的理論基礎。此外，通過預研的結果，組契約束求解還是降低計算複雜性的有效途徑之一，有望達到“1+1>2”的良好效果。因此，本項目還計畫研製相應的高效驗證工具包，供國內外同行借鑑。
結題摘要
現今信息技術已經滲透到日常生活的方方面面。如何提高信息計算系統的可靠性是一個不可迴避的問題。為了追求絕對正確性，相關的驗證離不開判定過程、約束求解方法。本項目首先重點研究各種複雜約束的求解算法，如 (i) 一類帶有指數函式的公式的量詞消去和 (ii) 將多項式次數從正整數推廣到實代數數的廣義多項式的正根隔離；其次，將它們有機地結合起來，並服務於計算系統的驗證領域，如 (i) 可解動力系統的軌跡問題和 (ii) 馬爾科夫報酬模型上的機率計算問題，都取得了良好的結果。在該項目支持下，我們發表了6篇高質量學術論文，其中：2篇發表在J. Symb. Comput.、2篇發表在Theoret. Comput. Sci.、1篇為ISSAC-2016，均第一標註本項目，圓滿完成原定研究目標；我們還培養在讀研究生4名（1名轉博、在讀3名）。根據國際上的最新熱點，建議後續工作可由從確定性的計算模型轉向機率性的計算模型，以期取得豐碩成果。
