SV 1 — Abstractions from Proofs
原文：POPL 2004 · doi:10.1145/982962.964021
這頁目前是骨架。 各節內容由 #3（前置補完）與 #4（論文本體）填上，手算題見 #5。現在放的是節標題與大綱，用來確認版面。
0 你需要先會的東西
這一節從零講起，不會叫你去讀別的資料再回來。會鋪的東西：
- 命題邏輯與一階邏輯的最小必要集合
- 什麼叫 satisfiable 與 unsatisfiable，SAT solver 到底在做什麼
- 一段 C 程式的執行路徑，怎麼變成一條邏輯公式
- 線代類比橋：$\sqsubseteq \approx \subseteq$、$\sqcup \approx \mathrm{span}$、fixpoint $\approx Ax = \lambda x$、abstraction $\approx$ 投影
先看一段程式：
int x = 1;
int y = x + 1;
if (y < 0) { ERROR; } // 到得了嗎？
你一眼就看得出 ERROR 到不了，因為 y 一定是 2。那電腦要怎麼自動看出來？這一問就是整篇 POPL'04 的入口。
1 這篇要解決的問題
三句話講完問題本身。待 #4。
2 在這之前人們怎麼做
CEGAR 的迴圈長什麼樣，以及它的痛點：predicate 要從哪裡來。前人的做法會讓 predicate 集合爆炸，驗證器跑不動。待 #4。
3 關鍵洞察
用 Craig interpolation 從 infeasible path 的「無解證明」裡，把 predicate 直接抽出來；而且是 per-location 的——不同的程式位置用不同的 predicate 集合，不是全域共用一大包。
這個洞察為什麼有效，跟 interpolant 的一個性質有關：它只會用到前後兩段公式共同出現的變數。待 #4。
4 手算一遍
這一節你要自己動手。給定一條走不通的路徑，一步一步算出它的 interpolant：
$$x_1 = 1 \;\wedge\; y_1 = x_1 + 1 \;\wedge\; y_1 < 0$$五個步驟，答錯會即時提示，答對才解鎖下一步。待 #5。
5 對後續的影響
這篇的實作是 BLAST。更重要的是，它後來被收進 SV 2 的 CPA 框架，成為其中一種 configuration——這條線在 SV 3 會收束。待 #4。
6 讀原文時的導覽
哪幾節必讀、哪幾節可以先跳過、台大校內網路怎麼取得。待 #4。