發(fā)布時間：2018-12-29 20:48

【摘要】：形式化驗證方法被認為是一種構(gòu)建高可信軟件系統(tǒng)的有效手段.在定理證明工具通過手動寫證明腳本來驗證系統(tǒng)軟件的功能正確性,這種驗證方式表達力強,可以證明復雜系統(tǒng),但是自動化程度低、驗證代價比較高;而使用程序驗證器接受經(jīng)過規(guī)范標注的源代碼生成驗證條件,并將驗證條件交給約束求解器自動求解,這種方式自動化程度高,缺點在于它很難驗證復雜系統(tǒng)軟件的全部功能的正確性.結(jié)合上述兩種方式的優(yōu)點,在定理證明工具Coq中實現(xiàn)了一個自動證明策略smt4coq,它通過在Coq中調(diào)用約束求解器Z3自動證明32位機器整數(shù)相關的數(shù)學命題,提高了自動化驗證的程度,減少了用戶手動驗證程序的開銷.
[Abstract]:Formal verification method is considered to be an effective method to construct high trusted software system. In theorem proving tool, the function correctness of the system software can be verified by manually writing the proof script. This verification method is expressive and can prove the complex system, but the automation degree is low, and the verification cost is high. The program validator is used to accept the standard annotated source code to generate the verification condition, and the verification condition is given to the constraint solver to solve it automatically. The drawback is that it is difficult to verify the correctness of all functions of complex system software. Combining the advantages of the above two methods, an automatic proof strategy, smt4coq, is implemented in the theorem proving tool Coq. By calling the constraint solver Z3 in Coq, we automatically prove the mathematical propositions related to 32-bit machine integers. It improves the degree of automatic verification and reduces the overhead of user manual verification program.
【作者單位】： 中國科學技術(shù)大學信息科學技術(shù)學院;中國科學技術(shù)大學計算機科學與技術(shù)學院;中國科學技術(shù)大學蘇州研究院軟件安全實驗室;
【基金】：國家自然科學基金(61103023,61229201,61379039,91318301,61632005)~~
【分類號】：TP311.52

【相似文獻】

相關期刊論文 前1條

1 何锫;證明策略及其有效性問題[J];軟件學報;1991年04期

相關碩士學位論文 前1條

1 曹景源;C程序證明策略在Coq中的設計和實現(xiàn)[D];中國科學技術(shù)大學;2015年

，

本文編號：2395377