2007 Clarke, Emerson & Sifakis —— 模型檢查：把「正確」交給機器#
「程式驗證要寫出『證明』，難如登天。三人換了一個問題： 能不能讓機器自己窮舉所有狀態，只告訴你『對/錯+反例』？ 這個『懶人的驗證』成為晶片工業的品管命脈。」
案件檔案#
| 項目 | 內容 |
|---|---|
| 得主 | Edmund M. Clarke (1945–2020)、E. Allen Emerson (1954–)、Joseph Sifakis (1946–) |
| 得獎理由 | 模型檢查的發明與發展：自動化驗證技術 |
| 關鍵詞 | CTL 模型檢查、狀態爆炸、反例生成 |
前因#
1981 年前，驗證的兩條路都堵死：
| 路線 | 方法 | 困境 |
|---|---|---|
| 演繹驗證（Hoare/Floyd） | 人寫證明 | 成本高、需數學家 |
| 測試 | 跑樣本 | 永遠不完備 |
Clarke 在 CMU 與博士生 Emerson、巴黎的 Sifakis 幾乎同時 （1981）提出第三條路。
線索與推理#
線索一：模型檢查的基本式#
輸入：系統模型 M（有限狀態轉移系統，Kripke 結構）
規格 φ（時態邏輯公式，Pnueli 1996 案的語言）
輸出：M ⊨ φ ？ 若否，給出反例執行軌跡
演算法（CTL 符號版）：
Sat(EX φ) = pre(Sat(φ)) （前驅像）
Sat(E[φ U ψ]) = lfp(Z. Sat(ψ) ∪ (Sat(φ) ∩ pre(Z)))
不動點迭代 → 線性於 |M|·|φ|
「驗證=圖上不動點計算」——把哲學問題變成圖論題。
線索二：狀態爆炸與三大解藥#
n 個並行元件 → 狀態數 Π|Sᵢ|（指數）。對策：
- 符號模型檢查（McMillan 1990，OBDD）：狀態集合用 布林函式表示，布林操作取代枚舉——壓縮率常達天文數字 （可處理 10²⁰ 以上狀態）
- 偏序約簡：交錯順序等價類只探其一
- 抽象化（counterexample-guided refinement, CEGAR）： 粗模型驗證→反例是假的→自動細化，循環收斂
線索三：Sifakis 的時態與分散式貢獻#
Sifakis（Verimag）把驗證帶進時間自動機（Timed Automata 與 Alur–Dill 的 UPPAAL 譜系）與分散式嵌入式 系統——「時間也是狀態」的推廣。
線索四：工業化的臨界點#
1990s 奇異（Clarke 的學生 Kurshan 的 COSPAN）、摩托羅拉、 英特爾（Firmware bug 的 Pentium FDIV 慘案 1994 是催化劑） 採用。今日晶片 tape-out 前的 formal verification 是 強制流程。
理論評析#
模型檢查的哲學翻轉：
演繹法：人證明機器 → 證明是「稀缺資源」
模型檢查：機器證明給人 → 證明是「自動計算」
代價：只能處理有限狀態；獎勵：反例即除錯線索
複雜度：CTL 模型檢查 O(|M|·|φ|) 線性——驗證問題裡 罕見的多項式，這是它可工業化的根本原因。
後果#
- 工具：SPIN、NuSMV、UPPAAL、CBMC、TLA+ 工具組 （Lamport 2013 案）、AWS 雲端協定驗證。
- 擴張到軟體：軟體模型檢查（SLAM、Java PathFinder）。
關聯案件#
→ 1996-Amir-Pnueli與時態邏輯、2013-Leslie-Lamport與分佈式系統及Paxos、1980-C.A.R.-Hoare與程式語言理論及CSP