[發(fā)明專利]基于SMT求解器的一階邏輯公式程序驗證方法及系統(tǒng)

在審

• 申請?zhí)枺?/td>: 202011055948.9
• 申請日: 2020-09-29
• 公開（公告）號: CN112231205A
• 公開（公告）日: 2021-01-15
• 發(fā)明（設(shè)計）人: 王浩;紀(jì)金龍;都云鑫
• 申請（專利權(quán)）人: 安徽中科國創(chuàng)高可信軟件有限公司;科大國創(chuàng)軟件股份有限公司
• 主分類號: G06F11/36
• 分類號: G06F11/36;G06F16/242;G06F16/2453
• 代理公司: 合肥維可專利代理事務(wù)所(普通合伙) 34135
• 代理人: 吳明華

本發(fā)明公開了一種基于SMT求解器的一階邏輯公式程序驗證方法及系統(tǒng)，包括接收至少一個客戶端中任一客戶端發(fā)送的程序形式化驗證數(shù)據(jù)交互請求；基于獲取的數(shù)據(jù)驗證請求內(nèi)容，提取數(shù)據(jù)驗證請求中的一階邏輯公式；基于SMT求解器對上述數(shù)據(jù)驗證請求中的一階邏輯公式進(jìn)行可滿足性求解。本發(fā)明基于SMT求解器實現(xiàn)了一階邏輯公式的自動證明，使得形式化驗證系統(tǒng)能夠?qū)Τ绦蜻M(jìn)行自動化驗證，提高軟件的可信度。

技術(shù)領(lǐng)域

本發(fā)明涉及計算機(jī)證明方法的技術(shù)領(lǐng)域，具體涉及一種基于SMT求解器的一階邏輯公式程序驗證方法及系統(tǒng)。

背景技術(shù)

基于演繹推理的形式化驗證主要用于提高軟件的可信度，在形式化驗證系統(tǒng)的驗證過程中，會產(chǎn)生大量的一階邏輯公式。通過證明一階邏輯公式的正確性，來證明程序的行為是否符合程序員的形式化描述，進(jìn)而證明程序的正確性。

現(xiàn)有技術(shù)中，why3和boogie在程序驗證領(lǐng)域使用都比較廣泛，其主要作為程序驗證工具的中間層，程序驗證工具將驗證得到的一階邏輯公式轉(zhuǎn)換為WhyML或Boogie語言描述，然后再通過將WhyML或者Boogie語言轉(zhuǎn)換為OCaml或者SMT2語言，再調(diào)用自動定理證明器證明。其中WhyML和Boogie語言語法復(fù)雜，學(xué)習(xí)曲線大，并且WhyML和Boogie作為中間層語言，與驗證者在驗證工具中描述的形式化語言差異較大，例如frama-c在前端使用ACSL語言描述，其與WhyML差異較大，驗證者需要同時學(xué)習(xí)ACSL和WhyML語言，不利于減輕程序驗證者的負(fù)擔(dān)。同時將WhyML和Boogie轉(zhuǎn)換為后端自動定理證明器輸入語言O(shè)Caml或者SMT2時，轉(zhuǎn)換后的證明文件內(nèi)容可讀性較差，不利于用戶的讀取和理解。基于現(xiàn)狀，亟待開發(fā)一種基于SMT求解器的一階邏輯公式驗證方法及系統(tǒng)，用于C程序的驗證，實現(xiàn)自動定理證明。

發(fā)明內(nèi)容

為解決上述現(xiàn)有技術(shù)的中的不足，本發(fā)明的目的在于克服現(xiàn)有不足，提供基于SMT求解器的一階邏輯公式程序驗證方法及系統(tǒng)，基于SMT求解器實現(xiàn)了一階邏輯公式的自動證明，使得形式化驗證系統(tǒng)對程序進(jìn)行自動化驗證，提高軟件的可信度。

本發(fā)明的給出了一種基于SMT求解器的一階邏輯公式程序驗證方法，包括：

接收至少一個客戶端中任一客戶端發(fā)送的程序形式化驗證數(shù)據(jù)交互請求；

基于獲取的數(shù)據(jù)驗證請求內(nèi)容，提取驗證數(shù)據(jù)交互請求中的一階邏輯公式；

基于SMT求解器對上述驗證數(shù)據(jù)交互請求中的一階邏輯公式求解證明。

作為上述方案的進(jìn)一步優(yōu)化，基于SMT求解器對上述數(shù)據(jù)交互請求中的一階邏輯公式求解證明具體包括如下步驟：

提取一階邏輯公式：從驗證數(shù)據(jù)交互請求中獲取初始一階邏輯公式；

一階邏輯公式預(yù)處理：基于獲取的SCSL語言描述的一階邏輯公式進(jìn)行預(yù)處理，通過前端的語法分析生成中間語法樹AST，化簡一階邏輯公式，削減變量，并構(gòu)造一階邏輯公式的否命題作為證明目標(biāo)。

SMT2代碼生成處理：預(yù)處理后輸入一階邏輯公式，遍歷語法樹，遍歷不同的表達(dá)式節(jié)點，生成節(jié)點對應(yīng)的SMT2語句，并輸出到字符緩沖區(qū)(或文件緩沖區(qū))；

SMT求解器：使用SMT求解器對一階邏輯公式生成的SMT2語句進(jìn)行求解；

結(jié)果分析處理：基于SMT求解器對一階邏輯公式的證明結(jié)果進(jìn)行分析，構(gòu)建證明子目標(biāo)，將一階邏輯公式劃分為子目標(biāo)進(jìn)行求解；

輸出證明結(jié)果：輸出證明結(jié)果，若結(jié)果不通過，輸出未通過的子目標(biāo)的一階邏輯公式。

作為上述方案的進(jìn)一步優(yōu)化，在所述SMT2代碼生成處理中，引入引理輔助證明一階邏輯公式。并且實現(xiàn)了引理自動證明，用于對被引入的引理進(jìn)行自動證明，以保證被引入的引理不會影響一階邏輯公式證明的可靠性。