基于Z3的Coq自動(dòng)證明策略的設(shè)計(jì)和實(shí)現(xiàn)
發(fā)布時(shí)間：2018-12-29 20:48
【摘要】：形式化驗(yàn)證方法被認(rèn)為是一種構(gòu)建高可信軟件系統(tǒng)的有效手段.在定理證明工具通過(guò)手動(dòng)寫(xiě)證明腳本來(lái)驗(yàn)證系統(tǒng)軟件的功能正確性,這種驗(yàn)證方式表達(dá)力強(qiáng),可以證明復(fù)雜系統(tǒng),但是自動(dòng)化程度低、驗(yàn)證代價(jià)比較高;而使用程序驗(yàn)證器接受經(jīng)過(guò)規(guī)范標(biāo)注的源代碼生成驗(yàn)證條件,并將驗(yàn)證條件交給約束求解器自動(dòng)求解,這種方式自動(dòng)化程度高,缺點(diǎn)在于它很難驗(yàn)證復(fù)雜系統(tǒng)軟件的全部功能的正確性.結(jié)合上述兩種方式的優(yōu)點(diǎn),在定理證明工具Coq中實(shí)現(xiàn)了一個(gè)自動(dòng)證明策略smt4coq,它通過(guò)在Coq中調(diào)用約束求解器Z3自動(dòng)證明32位機(jī)器整數(shù)相關(guān)的數(shù)學(xué)命題,提高了自動(dòng)化驗(yàn)證的程度,減少了用戶(hù)手動(dòng)驗(yàn)證程序的開(kāi)銷(xiāo).
[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.
【作者單位】： 中國(guó)科學(xué)技術(shù)大學(xué)信息科學(xué)技術(shù)學(xué)院;中國(guó)科學(xué)技術(shù)大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院;中國(guó)科學(xué)技術(shù)大學(xué)蘇州研究院軟件安全實(shí)驗(yàn)室;
【基金】：國(guó)家自然科學(xué)基金(61103023,61229201,61379039,91318301,61632005)~~
【分類(lèi)號(hào)】：TP311.52
本文編號(hào)：2395377
[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.
【作者單位】： 中國(guó)科學(xué)技術(shù)大學(xué)信息科學(xué)技術(shù)學(xué)院;中國(guó)科學(xué)技術(shù)大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院;中國(guó)科學(xué)技術(shù)大學(xué)蘇州研究院軟件安全實(shí)驗(yàn)室;
【基金】：國(guó)家自然科學(xué)基金(61103023,61229201,61379039,91318301,61632005)~~
【分類(lèi)號(hào)】：TP311.52
【相似文獻(xiàn)】
相關(guān)期刊論文 前1條
1 何锫;證明策略及其有效性問(wèn)題[J];軟件學(xué)報(bào);1991年04期
相關(guān)碩士學(xué)位論文 前1條
1 曹景源;C程序證明策略在Coq中的設(shè)計(jì)和實(shí)現(xiàn)[D];中國(guó)科學(xué)技術(shù)大學(xué);2015年
，本文編號(hào)：2395377
本文鏈接：http://www.sikaile.net/kejilunwen/ruanjiangongchenglunwen/2395377.html
最近更新
教材專(zhuān)著
