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

原文：JAR 2018 · doi:10.1007/s10817-017-9432-6

這頁目前是骨架。 內容由 #9 填上。現在放的是節標題與大綱，用來確認版面。

0 你需要先會的東西

• induction —— 大一數學已經有，可以直接接上
• BMC 是什麼 —— 把程式展開 $k$ 步，變成一條 SAT 公式
• k-induction 和 BMC 差在哪

1 這篇要解決的問題

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

2 在這之前人們怎麼做

每個演算法有自己的實作、自己的 SMT solver、自己的 benchmark 設定。跨論文的效能比較因此不可靠。待 #9。

3 關鍵洞察

四種演算法都能在 SV 2 的 CPA 框架裡，表達成同一個 algorithm 的不同 configuration。

這裡也是三篇收束的地方：SV 1 的 predicate abstraction 就是其中一種設定。

另一半貢獻是方法論——同一個實作、同一個 SMT solver、同一組 benchmark，才談得上公平比較。待 #9。

4 手算一遍

同一支程式，分別用 BMC（$k=3$）和 k-induction 跑一次，看兩者展開的公式差在哪。待 #9。

5 對後續的影響

待 #9。

6 讀原文時的導覽

待 #9。