這個單元的材料投影片補充教材程式作業

SV 3 — A Unifying View on SMT-Based Software Verification

原文：JAR 2018 · doi:10.1007/s10817-017-9432-6 · 開啟原文 PDF ↗

這是三篇的收束點，而且它問了一個很不客氣的問題：

BMC、k-induction、predicate abstraction、IMPACT——這四個看起來完全不同的演算法，各有各的論文、各有各的工具、各有各的實驗數據。它們真的不同嗎？而且，那些數據可以互相比較嗎？

答案是：它們是同一個框架的四種設定，而且過去的比較大多不公平。

0 你需要先會的東西

0.1 一個關於數字的尷尬問題

假設論文 A 說他們的方法在 benchmark 上贏過方法 B 三倍。你該信嗎？

不一定。因為 A 和 B 通常是：不同的人、不同的實作、不同的 SMT solver、不同的程式語言、不同的前端 parser、不同的硬體。三倍的差距裡，有多少來自演算法本身？

這篇論文有一半的價值在這裡：把四個演算法放進同一份實作、用同一個 solver 跑，這時候的比較才有意義。

這也是為什麼「統一框架」不只是理論上漂亮——它是做出可信實驗的前提。

0.2 先回顧：SSA 與 path formula

SV 1 教過的東西這裡整篇都在用。快速複習：

一條執行路徑翻成公式時，每個變數的每個版本要有自己的名字：

i = 0;
i = i + 1;

$$i_0 = 0 \;\wedge\; i_1 = i_0 + 1$$

論文 §4（p.315）明說它用的是 skolemized notation based on SSA indices，理由是「比起把一堆變數存在量化掉，這樣好讀得多」。看到 $x_0, x_1, x_2$ 就是這回事。

0.3 BMC：把迴圈攤平

Bounded model checking 的想法非常直接：迴圈就展開它。

i = 0;
while (i < 3) { i = i + 1; }
assert(i == 3);

展開兩圈的路徑翻成公式：

$$i_0 = 0 \;\wedge\; i_0 < 3 \;\wedge\; i_1 = i_0 + 1 \;\wedge\; i_1 < 3 \;\wedge\; i_2 = i_1 + 1$$

沒有迴圈了，就是一條長長的公式，丟給 SMT solver。

有解 → 這條路走得通，如果它通往 ERROR 就是真的 bug
無解 → $k$ 步之內沒有 bug

注意 BMC 的先天限制：它只能說「$k$ 步之內沒事」，不能說「永遠沒事」。要證明程式完全正確，BMC 不夠。

0.4 k-induction：把歸納法用在程式上

你在大一數學學過歸納法：證 $P(0)$，再證 $P(n) \Rightarrow P(n+1)$，就得到所有 $n$ 都成立。

套到程式上：

base case：初始狀態是安全的
inductive step：安全的狀態走一步之後還是安全的

如果兩者都成立，程式就永遠安全——而且不需要展開迴圈。

問題是第 2 條經常不成立。很多性質不是 inductive 的：從某個安全狀態走一步可能離開你描述的安全區，即使實際上程式仍然正確。

k-induction 的解法是把假設加強：不只假設「上一步安全」，而是假設「連續 $k$ 步都安全」，再證第 $k+1$ 步安全。假設越強，能證的東西越多。

論文 §4.2（p.316）補充了一個實務要點：即使用了 k-induction，很多性質對任何 $k$ 都不成立，除非再加上輔助不變量（auxiliary invariants）。所以實作上還會搭配 data-flow analysis 之類的技術去生成這些不變量。

0.5 ARG：記住誰是誰的後繼

ARG（abstract reachability graph）就是把探索過程記下來的圖：節點是 abstract state，邊表示「這個是那個的後繼」。

論文 §2.2（p.305）說得很清楚：ARG 是由一個專門的 ARG CPA 維護的，它存的就是 predecessor–successor 關係。

為什麼需要它？ 因為找到誤報時，你得知道「這條錯誤路徑是怎麼走過來的」才能修。ARG 就是那份路徑紀錄。SV 1 的 refinement 也需要這個，只是那時沒給它名字。

0.6 precision：每個位置各自的精細度

SV 1 的核心觀察是「不同程式位置需要不同的 predicate」。這篇把那個觀察正式化成一個物件：precision（精度），寫作 $\pi$。

$\pi$ 是一個從程式位置映到predicate 集合的函數。$\pi(l_4) = \{x = y\}$ 的意思是「在位置 $l_4$，追蹤 $x = y$ 這個 predicate」。

這就是 SV 1 那張「每個位置一份清單」的表，被寫成了框架的一等公民。

以上是前置。接下來是論文本身。

1 這篇要解決的問題

兩個問題，一個理論一個實務：

BMC、k-induction、predicate abstraction、IMPACT 之間的關係到底是什麼？
它們的效能數據能不能公平比較？

第二個問題其實依賴第一個——只有先證明它們是同一個框架的不同設定，「其他變因都相同」的比較才做得出來。

2 在這之前，卡在哪裡

每個演算法有自己的實作、自己的 SMT solver、自己的 benchmark 設定。跨論文的效能比較因此不可靠：你永遠分不清差距來自演算法還是來自工程細節。

而 SV 2 的 CPA 框架雖然統一了 model checking 和 data-flow analysis，四個零件還裝不下這四個演算法。

3 關鍵洞察

3.1 先把框架撐大：CPA+ 與 CPA++

SV 2 的 CPA 是四元組。這篇用的是六元組（定義在 §2.2, p.302）：

$$\mathbb{D} = (D, \Pi, \rightsquigarrow, \mathsf{merge}, \mathsf{stop}, \mathsf{prec})$$

多出來的兩個：

$\Pi$ —— 所有可能 precision 的集合
$\mathsf{prec}$ —— precision-adjustment operator，可以在執行途中調整精度

這個擴充不是本篇提出的。 論文 p.302 說得很清楚：The CPAs defined in this work make use of the extension CPA+ (dynamic precision adjustment) [19]，而 p.304 的 Algorithm 1 標題直接寫 taken from [19]。[19] 是 Beyer、Henzinger、Théoduloz 的 Program analysis with dynamic precision adjustment（ASE 2008）——也就是 SV 2 同一批作者在兩篇之間的中繼站。本篇是採用它，真正新增的是下面的 CPA++。

而且資料結構也變了：waitlist 和 reached 裡放的不再是 abstract state $e$，而是 $(e, \pi)$ 的配對——每個狀態隨身帶著自己的精度。這是 lazy abstraction 能做到「不同位置不同精度」的結構基礎。

還有第三代。 論文 §3.4（p.314）再擴充一次，叫 CPA++（Algorithm 2），差別有四項：收 reached/waitlist 當輸入並回傳更新版、呼叫 abort 提早停止、prec 改成每產生一個新狀態就呼叫、以及展開前先嘗試 forced covering。

世代	定義	出處
CPA	$(D, \rightsquigarrow, \mathsf{merge}, \mathsf{stop})$	SV 2（CAV'07）
CPA+	$(D, \Pi, \rightsquigarrow, \mathsf{merge}, \mathsf{stop}, \mathsf{prec})$	ASE'08（本篇引為 [19]；定義見 p.302、Algorithm 1 見 p.304）
CPA++	同上，演算法加 `abort` 與 `fcover`	本篇 Algorithm 2, p.315

3.2 `blk`：什麼時候做 abstraction

這是最能說明問題的一個旋鈕。

做 abstraction 是有代價的：每做一次就要呼叫 SMT solver 去計算「在這組 predicate 下，當前狀態長什麼樣」。做得越頻繁，狀態越小越好管，但 solver 呼叫越多。

Adjustable-Block Encoding（ABE） 把「多久做一次」變成參數，由 block-adjustment operator blk 控制：

設定	何時做 abstraction	效果
$\mathsf{blk}^{never}$	從不	整支程式當成一個 block（whole-program encoding）
$\mathsf{blk}^{l}$	loop head 與 error location
$\mathsf{blk}^{lf}$	再加上 function call/return	近似 large-block encoding

$\mathsf{prec}$ 就是照著 blk 的指示動作（論文 §3.1, p.308）：

$$\mathsf{prec}_{\mathbb{P}}((\psi, l^\psi, \varphi), \pi, R) = \begin{cases}((\psi \wedge \varphi)^{\pi(l)}_{\mathbb{B}},\, l,\, \mathit{true}), \pi & \text{if } \mathsf{blk}((\psi,l^\psi,\varphi), l)\\ (\psi, l^\psi, \varphi), \pi & \text{otherwise}\end{cases}$$

看起來嚇人，但意思很簡單：blk 說「該做了」就做 abstraction，否則原封不動放行。

$\mathsf{blk}^{never}$ 有個有趣的後果：abstraction 永遠不做，$\mathsf{stop}$ 因此永遠無法讓一個 abstract state 覆蓋另一個，CFA 就會一直展開下去。聽起來像壞事——但那正是 BMC 要的行為。

3.3 BMC 的完整配方：`blk` 不是唯一的旋鈕

這裡要很小心，因為一個常見的說法是錯的。

不能說「調一個 blk 就從 predicate abstraction 變成 BMC」。論文 §4.1（p.315）列的 BMC 配方是四個零件一起：

$\mathsf{blk}^{never}$ —— whole-program encoding
$\mathsf{fcover}^{id}$ —— 不做 forced covering
Loop-Bound CPA $\mathbb{LB}$ —— 每個 loop head 配一個計數器，precision 就是 loop bound $k$。它的 transfer relation 刻意是 unsound 的：計數器到達 $k$ 時不產生後繼狀態，用這個方式擋掉超過 $k$ 圈的路徑
外層再包一個演算法 —— 在 CPA++ 跑完後檢查每個 abstract error state 的 path formula 是否 satisfiable。另可做 forward-condition check，判斷 $k$ 夠不夠大

而 predicate abstraction 走的是 CEGAR + refinement，是完全不同的外層流程。

為什麼這件事值得計較？ 因為論文最重要的立論是「公平比較」，而公平比較的前提正是其他變因都相同、只有一個變因不同。把差別過度簡化成「一個運算子」，反而讓這個立論站不住。

正確的說法是：這些演算法共用同一個框架和同一份實作，差別落在一組可以獨立調整的旋鈕上——blk、fcover、要不要掛 Loop-Bound CPA、外層走不走 CEGAR。blk 是其中最能說明問題的一個。

3.4 refine 的四個步驟

論文 §3.2（p.309）把 refinement 拆成四步，這個結構值得原樣記住：

Abstract-Counterexample Construction —— 從 ARG 回溯出抽象反例 $\langle e_0, \dots, e_n \rangle$
Feasibility Check —— 把每段的 block formula 串成一條 counterexample formula，丟一次 SMT query。有解就是真 bug，無解就是誤報
Interpolation —— 求 interpolant 序列（見下）
Refinement Strategies —— 兩種選擇：

策略	做法
IMPACT 式	把 $\tau_i$ 直接 conjoin 進對應的 abstraction formula，強化既有狀態
Predicate 式	抽出 interpolant 的 atoms 當 predicate，加進 precision，從 pivot state（第一個會受新精度影響的狀態）之後重新探索

3.5 從一個 interpolant 到一整個序列

這裡要修正一個容易產生的印象。SV 1 並不是「只求一個 interpolant」——它的 Locality 段早就在沿著 trace 的每個 cut-point 各求一個了。

這篇的新意是：把那一串提升為有明確定義的物件。給定 $\widehat{\varphi} = \langle \varphi_1, \dots, \varphi_n \rangle$，序列 $\langle \tau_0, \dots, \tau_n \rangle$ 叫做 inductive sequence of interpolants，如果：

$\tau_0 = \mathit{true}$ 且 $\tau_n = \mathit{false}$
$\tau_{i-1} \wedge \varphi_i \Rightarrow \tau_i$
$\tau_i$ 只用同時出現在 $\bigwedge_{j \le i} \varphi_j$ 與 $\bigwedge_{j > i} \varphi_j$ 的變數

第 2 條是關鍵。 它要求整串前後扣得起來：每一個 $\tau_i$ 都能從前一個加上這一段的公式推出來。

公平地說，SV 1 不是沒提過這件事。 它在 p.235 就寫了「From Equation 1 of Section 3, it follows that $\mathsf{SP}.(\hat\psi_i).op_{i+1}$ implies $\hat\psi_{i+1}$, for each $i$」——同一個性質，只是當成推論順帶帶過。這篇的新意是把它寫進定義：一串滿足這三條的 interpolant 從此是一個有名字的物件，可以被拿來當作演算法的輸入輸出規格。這條「歸納性質」讓整串 interpolant 變成一個可以往下傳遞的鏈條，而不只是各切點各自為政的一堆事實。

3.6 四個演算法的對照

這是論文 Table 1（p.324）的內容，四個欄位照原樣列出：

演算法	抽象公式表示	`blk`	refinement 策略	`fcover`
BMC	SMT	$\mathsf{blk}^{never}$	無	$\mathsf{fcover}^{id}$
k-induction	SMT	$\mathsf{blk}^{never}$	無	$\mathsf{fcover}^{id}$
predicate abstraction	BDD	e.g. $\mathsf{blk}^{l}$	Predicate refinement	$\mathsf{fcover}^{id}$
IMPACT	SMT	e.g. $\mathsf{blk}^{l}$	IMPACT refinement	e.g. $\mathsf{fcover}^{\textsc{Impact}}$

表格讀不出來的兩件事，補在這裡。

第一，BMC 和 k-induction 的 refinement 欄是「無」，因為它們不走 CEGAR，改由外層演算法驅動：BMC 外面包一層 satisfiability 檢查（還要掛 Loop-Bound CPA），k-induction 外面是 Algorithm 3（p.318），負責逐步加大 $k$ 並注入輔助不變量。

第二，論文寫的是「e.g.」，不是唯一解。predicate abstraction 和 IMPACT 的 blk 都標 e.g. $\mathsf{blk}^{l}$——§4.3（p.320）的要求只是 block 裡不能含潛在的無限路徑，$\mathsf{blk}^{l}$ 是符合條件的一個選擇。IMPACT 的 $\mathsf{fcover}^{\textsc{Impact}}$ 同樣標 e.g.，p.322 說它是「if desired ... as an optimization」——是選配，不是 IMPACT 的定義的一部分。

4 手算一遍

blk 的效果用算的比用讀的清楚。

5 對後續的影響

這篇是 CPAchecker 現在的理論骨架。 上面講的每個零件都對應到實作裡的一個 configuration 選項——四個演算法共用同一份程式碼，差別只在設定檔。

方法論上的影響可能更大。 這篇示範了一件事：要比較演算法，先把它們放進同一份實作、用同一個 solver。帶著這個標準，你之後讀任何驗證工具的論文都可以問一句：這個比較控制了哪些變因？

回頭看三篇的關係：

SV 1 (POPL'04)         SV 2 (CAV'07)              SV 3 (JAR'18)
predicate 從哪來   →   怎麼統一所有分析      →   統一後能公平比較什麼
Craig interpolation    CPA 四元組                 CPA+ / CPA++ 與一組旋鈕
       └──────── 是這個框架的一種設定 ────────┘

SV 1 給了一個具體技術，SV 2 給了一個框架，SV 3 把技術裝回框架裡並證明它跟其他技術是同類。這就是為什麼三篇該一起讀。

6 讀原文時的導覽

37 頁，是三篇裡最長的。不必一次讀完。

下表只列逐頁核對過的章節與起始頁。論文自己在 §1.4 Structure（p.301）交代了整體結構：§2 背景、§3 定義框架、§4 用框架表達四個方法、§5 實驗評估。

章節	頁	建議
§1 Introduction	p.299–301	必讀。動機與貢獻；§1.4 Structure 是全篇地圖
§2 Background	p.301–305	必讀。 §2.1 程式表示法、§2.2 CPA（p.302，含 CPA+ 六元組定義）、§2.3 CEGAR（p.305）
§3 Predicate CPA	p.305–315	必讀。 abstract state 的三元組結構、`blk`、`prec`
└ §3.2 Refinement	p.309	必讀。四個步驟與 interpolant 序列的定義
└ §3.3 Forced Covering	p.313	進階。IMPACT 的加速機制
└ §3.4 An Extended CPA Algorithm	p.314	值得看 Algorithm 2（CPA++）與那四項差異
§4 Unifying SMT-Based Approaches	p.315–326	挑著讀。四個方法各一節；四者的設定對照表 Table 1 在 p.324
└ §4.1 Bounded Model Checking	p.315	先讀這節就好，BMC 的完整配方在這
└ §4.2 k-Induction	p.316
└ §4.4 Lazy Abstraction with Interpolants (IMPACT)	p.322
§5 Evaluation	p.326 起	進階。公平比較的實際數據；benchmark 取自 SV-COMP'17

建議路徑：§1 → §2 → §3.1 → §3.2 → §4.1，其餘按需要再回頭。

取得原文：台大校內網路可直接下載，見頁首 DOI。

三篇到這裡結束。接下來的 hands-on 是把這些概念裝進真的工具裡——CPAchecker 的 config 選項，你現在應該看得懂大半了。