在2024-2025學期的巴黎高師同步反應式系統(2024-2025)第三課中，詳細討論了基于SMT的Lustre模型檢查器Kind 2的工作。本文將提供對Kind 2的介紹。對課程的詳細內容，可參考同步反應式系統

簡介

本節課討論了基于SMT（Satisfiability Modulo Theories）的轉換系統模型檢驗技術，涵蓋從基本概念到具體應用的多個方面。課程中討論了兩種性質：安全性和活性性質，并解釋了它們在系統驗證中的重要性。接著詳細介紹了SMT求解器的基礎知識，包括SAT求解器的發展歷程及其與SMT求解器的關系。隨后討論了模型檢驗的不同方法，如顯式狀態枚舉、基于BDD的算法、有界模型檢驗和k-歸納法等。特別地，文章深入探討了k-歸納法的具體實現和優化策略，包括路徑壓縮和抽象化技術。最后，介紹了用于Lustre程序的SMT模型檢驗工具Kind 2，展示了如何利用SMT技術進行形式化驗證。

Kind 2 介紹

Kind 2是一款基于SMT的開源多引擎自動模型檢查器，用于驗證以Lustre語言擴展形式表達的有限狀態或無限狀態同步反應系統的安全性屬性。在基礎配置中，該工具接收一個或多個標注了待證明不變屬性的Lustre文件作為輸入，并為每個屬性輸出確認結果或反例（即違反該屬性的輸入序列）。其高級功能包括基于合約的組合驗證、已證明屬性的證書生成，以及基于合約的測試用例生成。

核心功能

支持Lustre V4及部分V6語法特性：

• C風格機器整數的有符號/無符號版本
• If-Then-Else條件塊與Frame Condition塊
• 精化類型系統
• 基于假設/保證的合約語言
• 模塊化組合驗證
• 反例與證據生成
• 證明證書生成
• 通過以下計算進行優劣歸因分析：

歸納有效性核心(Inductive Validity Cores)

最小割集(Minimal Cut Sets)

• 合約可實現性與可滿足性檢查
• 針對不可實現合約的死鎖軌跡生成
• 非空虛性檢查：

條件屬性

合約模式蘊含關系

• 合約假設生成

多模型檢查引擎支持：

• 有界模型檢查(BMC)
• 帶惰性路徑壓縮的k歸納法
• IC3/PDR算法
• 基于模板的系統語法分析及不變式發現
• 基于消息傳遞的模型檢查引擎并行組合
• 基于圖的不變式生成
• 引擎間共享已發現不變式

后端推理引擎支持多種SMT求解器：
Bitwuzla、cvc5、MathSAT5、SMTInterpol、Yices 2、Yices 1及Z3

附加功能：

• 將可執行Lustre模型編譯為Rust代碼
• 測試用例生成

參考

• Kind 2: kind2-mc.github.io/kind2/
• 課程課件: 同步反應式系統第三課 - Kind 2: 基于SMT的Lustre模型檢查器