SV 2 — Configurable Software Verification
原文：CAV 2007 · doi:10.1007/978-3-540-73368-3_51
這頁目前是骨架。 內容由 #8 填上。現在放的是節標題與大綱，用來確認版面。
0 你需要先會的東西
- 什麼是 lattice —— 直接用線代的子空間包含關係類比
- 什麼是 fixpoint —— $F(x) = x$，對照你已經會的特徵向量 $Ax = \lambda x$
- data-flow analysis 在做什麼
1 這篇要解決的問題
model checking 和 program analysis 長期是兩個社群、兩套詞彙、兩種工具，但它們在做的事高度重疊。待 #8。
2 在這之前人們怎麼做
兩邊各自發展，難以互相借用彼此的最佳化。待 #8。
3 關鍵洞察
把兩者統一成一個四元組：
$$\mathbb{D} = (D, \rightsquigarrow, \mathsf{merge}, \mathsf{stop})$$其中 $D$ 是 abstract domain、$\rightsquigarrow$ 是 transfer relation、$\mathsf{merge}$ 決定何時合併 abstract state、$\mathsf{stop}$ 決定何時停止探索。
真正漂亮的地方是：只要調 merge 和 stop，就能在 model checking 和 data-flow analysis 之間連續滑動。
| 設定 | 行為 | 相當於 |
|---|---|---|
merge^sep | 路徑保持分離 | model checking |
merge^join | 相同位置的 state 合併 | data-flow analysis |
待 #8。
4 手算一遍
同一個 CFA，分別用 merge^sep 和 merge^join 跑一次，數數看 abstract state 各產生幾個。待 #8。
5 對後續的影響
這個框架就是 CPAchecker 的骨架，也是 SV 3 用來統一四種 SMT-based 演算法的基礎。待 #8。
6 讀原文時的導覽
待 #8。