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

在審

• 申請號: 202011055948.9
• 申請日: 2020-09-29
• 公開（公告）號: CN112231205A
• 公開（公告）日: 2021-01-15
• 發明（設計）人: 王浩;紀金龍;都云鑫
• 申請（專利權）人: 安徽中科國創高可信軟件有限公司;科大國創軟件股份有限公司
• 主分類號: G06F11/36
• 分類號: G06F11/36;G06F16/242;G06F16/2453
• 代理公司: 合肥維可專利代理事務所(普通合伙) 34135
• 代理人: 吳明華

1.基于SMT求解器的一階邏輯公式程序驗證方法，其特征在于，包括：

接收至少一個客戶端中任一客戶端發送的驗證數據交互請求；

基于獲取的數據驗證請求內容，提取驗證數據交互請求中的一階邏輯公式；

基于SMT求解器對上述驗證數據交互請求中的一階邏輯公式進行可滿足性求解。

2.根據權利要求1所述的基于SMT求解器的一階邏輯公式程序驗證方法，其特征在于，基于SMT求解器對上述驗證數據交互請求中的一階邏輯公式進行可滿足性求解，具體包括如下步驟：

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

一階邏輯公式預處理：基于獲取的SCSL語言描述的一階邏輯公式進行預處理，通過前端的語法分析生成中間語法樹AST，化簡一階邏輯公式，削減變量，并構造一階邏輯公式的否命題作為證明目標；

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

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

結果分析處理：基于SMT求解器對一階邏輯公式的證明結果進行分析，構建證明子目標，將一階邏輯公式劃分為子目標進行求解；

輸出證明結果：輸出證明結果，若結果不通過，輸出未通過的子目標的一階邏輯公式。

3.根據權利要求2所述的基于SMT求解器的一階邏輯公式程序驗證方法，其特征在于，在所述SMT2代碼生成處理中，引入引理輔助證明，并且實現了被引入引理的自動證明。

4.根據權利要求3所述的基于SMT求解器的一階邏輯公式程序驗證方法，其特征在于，引理自動證明中，設置前驅引理和目標引理，前驅引理用來對目標引理進行輔助證明；并通過語法定義了前驅引理和目標引理間的依賴關系。

5.根據權利要求2所述的基于SMT求解器的一階邏輯公式驗證方法，其特征在于，所述一階邏輯公式預處理包括：

語法樹AST生成:通過前端的語法分析將一階邏輯公式生成中間語法樹AST；

消減變量：對一階邏輯公式中的常量進行代換；對一階邏輯公式中相等變量，用同一變量進行代換；

常量表達式計算：對于一階邏輯公式中的可計算的常量計算表達式進行計算；

移除重復布爾型子式：移除一階邏輯公式中的重復布爾(bool)型子式；

斷言拆分和拼接：對于一階邏輯公式中的量化斷言嘗試拆分和拼接處理；

證明目標構造：構造一階邏輯公式的否命題作為證明目標邏輯公式。

6.根據權利要求2所述的基于SMT求解器的一階邏輯公式程序驗證方法，其特征在于，所述引理自動證明包括：

構建引理集合；

分析引理間的依賴關系，對引理集合進行排序；

按照順序對引理進行證明，按照歸納證明原理構造歸納假設；

將構造的歸納假設，調用SMT2代碼生成器，將歸納假設的一階邏輯公式轉換為SMT2語句，再使用SMT求解器證明；

輸出引理證明結果。

7.根據權利要求2所述的基于SMT求解器的一階邏輯公式程序驗證方法，其特征在于，所述結果分析處理包括：

若SMT求解器返回的結果值為不滿足，直接輸出待驗證一階邏輯公式的證明結果為真；

若SMT求解器返回的結果值為滿足或未知，拆分待驗證一階邏輯公式的蘊含式右件為合取子式，構建新的一階邏輯公式作為證明子目標；

求解證明新構建的子目標：

若所有子目標證明結果為通過，輸出待驗證一階邏輯公式的證明結果為真；

若存在部分子目標未通過，輸出待驗證一階邏輯公式的證明結果為假，且將未通過的子目標輸出。