Hands-on — 把概念裝進真的工具
三篇論文讀完之後，這一頁把概念接到真正跑得動的東西上。
這一頁的指令全部來自各工具的官方 README，但我沒有在你的機器上實際跑過。 版本會變，環境會不同——遇到落差時以官方文件為準，並且回報給我修正。每一節都附了原始出處。
0 先看一眼三個工具的關係
| 工具 | 輸入 | 做法 | 對應教材 |
|---|---|---|---|
| CPAchecker | C 程式 | 直接在軟體層做 configurable program analysis | SV 2 的框架本尊、SV 3 的實作平台 |
| CPV | C 程式 | 先翻成硬體電路（Btor2），交給硬體 model checker | SV 3 的延伸：換一個完全不同的後端 |
| MoXIchecker | MoXI 模型 | 直接檢查中介語言，不經過 C | 另一條路：統一的不是演算法而是輸入格式 |
三者都出自 sosy-lab（也就是 SV 2、SV 3 的作者群）。這不是巧合——SV 2 的框架讓「換零件」變得便宜，這三個工具就是換不同零件的結果。
環境方面先有心理準備：這三個都以 Linux 為主要平台。macOS 上 CPAchecker 的預設設定需要自己編 MathSAT，CPV 直接要求 Ubuntu 22.04+。用 Docker 或實驗室的 Linux 機器最省事。
1 CPAchecker
1.1 它是什麼
SV 2 定義的 configurable program analysis，實作出來就是這個工具。SV 3 講的四個演算法，也全部在這裡面。
換句話說：你讀的兩篇論文，程式碼在這裡。
1.2 安裝
官方提供三條路（見 INSTALL.md）：
# 路徑 A：Debian/Ubuntu 套件（最省事）
# 先照 https://apt.sosy-lab.org/ 的說明啟用 SoSy-Lab APT repo，然後：
sudo apt install cpachecker
# 路徑 B：ZIP 檔
# 需要 Java 21 以上
sudo apt install openjdk-21-jre
# 路徑 C：容器映像（macOS 建議走這條）
Java 21 是硬性需求。 如果 java 不在 PATH 裡，要指定環境變數：
export JAVA=/usr/lib/jvm/java-21-openjdk-amd64/bin/java
官方建議至少 Ubuntu 24.04 或 Debian 13，才能完整支援現代 SMT solver。
1.3 跑第一個例子
repo 自帶範例，不必自己找程式：
bin/cpachecker doc/examples/example.c
這是預設設定。doc/examples/example.c 長這樣（節錄）：
int main() {
int i = 0;
int a = 0;
while (1) {
if (i == 20) { goto LOOPEND; }
else { i++; a++; }
if (i != a) { goto ERROR; }
}
...
}
i 和 a 每圈同步加一，所以 i != a 永遠不成立，ERROR 到不了。但要證明這件事，驗證器必須發現不變量 i == a——這正是 SV 1 在解的問題（那個事實從哪裡來），也是 SV 3 的 refinement 在做的事。
另外有一個帶 bug 的版本 doc/examples/example_bug.c 可以對照，看工具找到反例時的輸出長什麼樣。
規格檔預設是 config/specification/default.spc，它會去找名為 ERROR（不分大小寫）的標籤和 assertion。所以上面那支程式不需要額外指定規格。
1.4 config 檔名就是教材的索引
這是這一節最值得看的地方。CPAchecker 的 config/ 目錄有 90 幾個設定檔，而檔名直接對應你讀過的論文概念：
config/predicateAnalysis-ImpactRefiner-ABEl.properties
└──── SV1 / SV2 ────┘└─ SV3 §3.2.4 ─┘└ SV3 §3.1 ┘
predicate abstraction IMPACT 式 refinement blk^l
一個檔名把三篇論文串起來了。 拆開來看：
| 檔名片段 | 是什麼 | 出處 |
|---|---|---|
predicateAnalysis | predicate abstraction | SV 1 全篇、SV 2 §2.3 的 instance |
ImpactRefiner | IMPACT 式的 refinement 策略——把 interpolant 直接 conjoin 進 abstraction formula | SV 3 §3.2.4 |
ABEl | adjustable-block encoding 配 $\mathsf{blk}^{l}$，也就是只在 loop head 與 error location 做 abstraction | SV 3 §3.1 |
其他值得試的設定（全部真實存在於 config/）：
| 設定檔 | 對應教材 |
|---|---|
bmc.properties | SV 3 §4.1 的 BMC |
bmc-incremental.properties | BMC 逐步加大 $k$ |
bmc-incremental-ABEl.properties | BMC 但改用 $\mathsf{blk}^{l}$——親手轉那個旋鈕 |
bmc-induction.properties | SV 3 §4.2 的 k-induction |
bmc-interpolationSequence.properties | SV 3 §3.2.3 的 inductive interpolant 序列 |
combinations-bdd+impact.properties | IMPACT 與 BDD 的組合 |
指定設定的兩種寫法（等價）：
bin/cpachecker --config config/bmc.properties doc/examples/example.c
bin/cpachecker --bmc doc/examples/example.c
1.5 建議的練習
- 先用預設設定跑
example.c，確認環境沒問題 - 換成
bmc.properties跑同一支程式。想想看它憑什麼給出結論——BMC 只保證 $k$ 步之內，那它對一個無界迴圈能說什麼？ - 換成
bmc-incremental-ABEl.properties。這一步你就親手把 $\mathsf{blk}$ 從never轉到l了 - 跑
example_bug.c，看反例輸出長什麼樣
第 2 步的疑問，正是 SV 3 §4.1 那個 forward-condition check 在回答的。
2 CPV
2.1 它是什麼
Circuit-based Program Verifier——把 C 程式翻成硬體電路，然後用硬體 model checker 去驗。
這聽起來很繞，但想法很直接：硬體驗證領域有幾十年的工具累積（ABC、AVR、Pono、rIC3），如果能把軟體問題翻譯過去，就能免費繼承那些工具的所有進步。
架構是這樣（見 README）：
C 程式 ──▶ Instrumentor ──▶ Kratos2 ──▶ Btor2 電路
│
硬體 model checker
(ABC / AVR / Pono / rIC3)
│
Btor2 witness ──▶ 翻譯回軟體 ──▶ SV witness
中間的 Kratos2 負責 C → 電路的翻譯，CoVeriTeam 負責協調後端的硬體驗證器。
注意 Btor2 就是暑訓 HWMC 主題在讀的那個格式（CAV 2018）。這裡是兩個主題的交會點。
2.2 系統需求
比另外兩個嚴格：
- Linux Ubuntu 22.04 或更新
- Python 3.10 或更新
- cgroups（CoVeriTeam 用來控制資源）
apt-get install clang clang-format clang-tidy cpp python3 \
python3-bitstring python3-lxml python3-pycparser
還要注意：後端的硬體 model checker 各自有自己的系統需求。
2.3 安裝與執行
# 要連同 submodule 一起 clone
git clone --recurse-submodules https://gitlab.com/sosy-lab/software/cpv.git
cd cpv
./scripts/setup.sh # 下載並解壓 Kratos2
如果從 Zenodo 下載打包好的 tool archive，上面的 setup 可以跳過。
執行：
./bin/cpv --property <prp_file> --model {ILP32,LP64} <c_prog>
--model 指定資料模型（32 或 64 位元），--property 指定要驗的性質（可從 sv-benchmarks 取得標準的 property 檔）。
同時跑多個 CPV 實例時，記得用
--output-dir分開輸出目錄，否則會互相衝突。
2.4 這跟你讀的論文有什麼關係
SV 3 證明了四個軟體驗證演算法是同一個框架的不同設定。CPV 把這個想法再推一步：連「要不要留在軟體領域」都可以是一個設定。
翻成電路之後，你能用的後端從「SMT solver」變成「所有硬體 model checker」。SV 3 的公平比較方法論在這裡同樣適用——只是被比較的對象換成了不同的硬體引擎。
3 MoXIchecker
3.1 MoXI 是什麼
MoXI = Model eXchange Interlingua（定義見這篇），一個模型檢查的中介語言。
它想解決的問題跟 SV 3 有點像，但切入點不同：
- SV 3 統一的是演算法——把四種方法放進同一個框架
- MoXI 統一的是輸入格式——讓不同的 model checker 讀同一種模型描述
有了共通格式，工具之間就能互換，也才談得上公平比較。
3.2 MoXIchecker 是什麼
一個可擴充的 MoXI model checker。用 Python 寫，靠 PySMT 操作與求解 SMT 公式。目前支援 QF_BV、QF_ABV、QF_LIA、QF_NIA、QF_LRA、QF_NRA 這幾個理論。
它的架構刻意做得很薄：
MoXI 模型 (JSON) ──▶ moxi2smt.py ──▶ init / trans / inv / query
（公式抽取） （PySMT 公式）
│
model_checking.py
（檢查引擎）
│
reachable / unreachable
「可擴充」是重點：因為公式抽取和檢查引擎分開了，要加一個新的 model-checking 演算法，只需要動 model_checking.py。這跟 SV 2 「把零件抽出來就能替換」的思路完全一致，只是換了一個層次。
3.3 安裝與執行
需要 Python 3.10 以上。建議用 venv 或 Python container 隔離環境：
pip install setuptools pysmt==0.9.7.dev333
pysmt-install --msat --z3 # 官方建議 MathSAT 與 Z3 這兩個後端
執行：
./bin/moxichecker <moxi-json-file>
# 例如 repo 自帶的：
./bin/moxichecker examples/QF_ABV/count2.moxi.json
或用容器（免安裝）：
podman run -v $(pwd):/workdir \
registry.gitlab.com/sosy-lab/software/moxichecker <moxi-json-file>
一個限制要知道：MoXIchecker 目前只分析單一個 reachability query。如果模型裡有多個
check-system或多個查詢條件，只有第一個會被處理，其餘會印警告跳過。
./bin/moxichecker -h 有完整選項。
4 三條路，同一個問題
三個工具在做同一件事——判斷某個狀態到不到得了——但走的路完全不同：
| 表示方式 | 求解引擎 | |
|---|---|---|
| CPAchecker | abstract state + precision | SMT solver |
| CPV | Btor2 電路 | 硬體 model checker |
| MoXIchecker | MoXI 模型 | PySMT + SMT solver |
共同點是那個貫穿三篇論文的觀念：把「用什麼零件」變成可替換的參數。 SV 2 把它用在演算法內部（merge / stop），SV 3 用在演算法之間（blk / fcover / CEGAR），CPV 用在整個問題領域之間（軟體 / 硬體），MoXIchecker 用在輸入格式上。
看懂這一層，這三個工具就不是三個要分別學的東西，而是同一個設計哲學的三次應用。
練習建議：如果時間有限，只做 CPAchecker 那一節的四個步驟。跑通 bmc-incremental-ABEl.properties 的那一刻，你會親眼看到論文裡那個 $\mathsf{blk}$ 運算子在真實工具裡長什麼樣。