Graf-Saïdi — 用谓词把无限状态压成有限抽象

是什么

谓词抽象（predicate abstraction）是一种把巨大或无限的程序状态空间压成有限张表的方法。Graf 和 Saïdi 1997 年的论文第一次把它做完整：你提供一组逻辑判断句，机器替你算出抽象后的状态图。

日常类比：体检报告。一个人具体有几千项指标（身高 173.2cm、血压 124/82……），但医生不会每项都看，他用三五个判断句——“BMI 正常吗 / 血压高吗 / 血糖高吗”。每个判断只有是 / 否两种答案，三个问题就把所有人压成 8 个类别。同一类别的人医生给同一种处方。

把”病人”换成”程序状态”，“判断句”换成”谓词”，就是谓词抽象。比如一个变量 x 是 32 位整数，本来有 2^32 种取值，你只问 x > 0、x = 0 两个谓词，立刻压成 3 类（正 / 零 / 负）。

为什么重要

不理解 Graf-Saïdi，下面这些事都没法解释：

为什么 SLAM / BLAST / SatAbs / CPAchecker 这些验证工具都说自己是”基于谓词抽象”——它们的根源就是这篇 1997 年的论文
为什么 Microsoft 2002 年能自动验证 Windows 设备驱动——SLAM 把谓词抽象 + CEGAR 闭环工程化
为什么”用定理证明器算抽象”是个发明——之前抽象解释的抽象域要数学家手设计
为什么clarke-cegar-2003 论文里反复提”Graf-Saïdi 的抽象”——CEGAR 是它的自动化升级版

核心矛盾：cousot-abstract-interpretation 1977 给了抽象框架，但每个程序都要重新设计抽象域。Graf-Saïdi 给出一个通用模板——抽象域永远是”谓词的布尔组合”，剩下的工作交给定理证明器。这把”专家手艺”变成了”流水线作业”。

核心要点

谓词抽象分三步：

选谓词：人提供一组判断句 P = {p1, p2, …, pn}。每个 pi 是个具体状态上的布尔表达式，例如 x > 0、p == NULL、lock_held。
抽象状态 = 布尔向量：每个具体状态 s 对应 n 位向量 (p1(s), p2(s), …, pn(s))。最多 2^n 个抽象状态。所有让谓词取相同值的具体状态被合并到同一抽象状态。
抽象转移 = 问 PVS：对每对抽象状态 (b, b’)，问定理证明器 PVS：“存在具体 s ∈ b 使得 s 走一步能到 s’ ∈ b’ 吗？“PVS 答是 / 否 / 不知道。算完所有 2^n × 2^n 对，得到抽象转移图。

得到的图用普通模型检查器（如 SMV）跑——状态数有限，能用。

关键性质：这是过近似——具体程序能走的转移，抽象图里一定也有；抽象图里有的，具体程序未必有。所以”抽象证安全 = 原程序安全”，但”抽象有反例 ≠ 原程序有 bug”（伪反例问题）。

实践案例

案例 1：一个最小例子

int x = 0;
while (x >= 0) x = x + 1;

具体状态空间：x 取所有 32 位整数，加上溢出。直接验证太大。

选两个谓词：p1 = (x ≥ 0)，p2 = (x = 0)。抽象后只有 4 个布尔向量，实际可达 3 个：(T, T)、(T, F)、(F, F)。

问 PVS：(T, T) → ? 能到哪些状态。PVS 答：x = 0 加 1 后 x = 1，对应 (T, F)。再问 (T, F) → ? 答：可能继续 (T, F)，也可能溢出到 (F, F)。

抽象图画完，用模型检查器看 (F, F) 可不可达——结论”可达”，意味着 x 能变负。原程序对应”溢出后变负”，确认。

案例 2：为什么必须用 PVS（或类似工具）

抽象转移这一步 PVS 在做的事，本质是自动证明蕴含式：

{p1 = T, p2 = T} ∧ stmt   ⟹   {p1' = T, p2' = F}

也就是”在 p1 真 p2 真时执行这条语句，结果是不是必然 p1 真 p2 假”。这个判断是个一阶逻辑问题，要解线性算术 / 数组 / 指针等理论。手算几百对状态会写到崩溃，PVS 能在秒级单次解决。

后来 SatAbs（2005）发现很多场景下 SAT 求解器替代 PVS 速度快十倍，但底层逻辑没变。

案例 3：抽象信息丢得多猛

考虑 x = x * 2，谓词只有 p = (x > 0)。

具体语义：x = 5 → x = 10，x = -3 → x = -6。

抽象：(p = T) → (p = T)，(p = F) → (p = F)。但 x = 0 呢？(p = F) → (p = F)。

如果原程序里 x 必须乘到 100 以上才出 bug，谓词 p 完全捕捉不到。这时谓词太粗，得加更细的——比如 p2 = (x > 50)。选谓词是个手艺活——这正是 5 年后 CEGAR 要解决的痛点。

案例 4：和后续工具的关系

工具	年份	在 Graf-Saïdi 上加了什么
SLAM	2002	+ CEGAR 闭环 + Windows 驱动专用谓词模板
BLAST	2003	+ lazy abstraction（不同程序点用不同谓词）
SatAbs	2005	+ 用 SAT 替代 PVS 加速
CPAchecker	2011	+ 多种抽象域可插拔 + 现代 C 前端

每个工具的核心循环里都有”用谓词把状态压成布尔向量”这一步——那一步就是 Graf-Saïdi。

踩过的坑

谓词全靠手选：原始 Graf-Saïdi 没有自动谓词发现。专家拍脑袋写出 5 个谓词跑一轮发现不够，再加 2 个，反复试。直到 clarke-cegar-2003 才用反例驱动这个过程。
PVS 调用很慢：每对抽象状态都要一次定理证明，n 个谓词产生 2^n × 2^n = 4^n 次调用。10 个谓词就是百万次。后来用 SAT 替代 / 增量计算 / 缓存一致性才让大程序跑得动。
过近似太松：谓词不够时抽象图里全是伪转移，模型检查输出一串”可能有 bug”的反例，人去验证发现全假。这种”假阳性”让早期工具不实用。
不能跨过程：原始算法假设单过程程序。函数调用要扩展为”过程内 + 过程间摘要”，复杂度上一台阶。SLAM 的工程突破之一就是把这个做对了。

适用 vs 不适用场景

适用：

控制流复杂、数据简单的程序——驱动、协议、操作系统组件
安全性属性’某个 ERROR 状态不可达’
中等规模程序（百级谓词）
已有定理证明器或 SMT 后端的环境

不适用：

数据密集程序（数值计算、ML 训练）—— 谓词没法捕捉浮点 / 矩阵关系
活性属性’A 终会发生’—— 要扩展成 progress measure
高度依赖具体堆形状的程序 —— 用sagiv-shape-analysis 形状分析更合适
谓词无法预先想清楚的程序 —— 要 CEGAR 闭环

历史小故事（可跳过）

1977 年：Cousot 夫妇提出抽象解释，给所有静态分析一个数学框架。但抽象域要逐题手设计。
1993 年：PVS 定理证明器在 SRI 完成。能自动判定一阶逻辑加常见理论。
1997 年：Graf 在 Verimag、Saïdi 在 SRI 合作，把”抽象域 = 谓词布尔组合”这个具体模板敲定，把抽象转移交给 PVS。这就是本论文，CAV 1997。
2000 年：Clarke 团队意识到”谓词手选”是工程瓶颈，发明 CEGAR 自动化它。
2002 年：Microsoft Ball-Rajamani 把谓词抽象 + CEGAR 做成 SLAM，验证上千个 Windows 驱动找出几百 bug。商业上一战封神。
2007 年：Clarke / Emerson / Sifakis 拿图灵奖，Graf-Saïdi 作为 enabling technology 被反复引用。

学到什么

抽象的关键是选对模板——Cousot 给了”什么是抽象”的数学，Graf-Saïdi 给了”怎么落地的工程模板”，差别就是后者立刻能写出工具
过近似 + 自动求解是验证系统的通用配方——丢点信息换可判定，让定理证明器替你算
谓词的强大是它能编码任何性质——“锁拿了 / x 是空指针 / i 在数组范围内”都是一个布尔表达式
理论 → 工具 → 工业：1977 抽象解释 → 1997 谓词抽象 → 2002 SLAM。25 年才把概念落到产品

关联

clarke-cegar-2003 —— CEGAR 在 Graf-Saïdi 之上加了反例驱动循环，让谓词自动发现
cousot-abstract-interpretation —— 抽象解释提供数学框架，谓词抽象是它的具体模板
slam-microsoft —— SLAM 把 Graf-Saïdi + CEGAR 工程化到 Windows 驱动
biere-bmc-1999 —— 兄弟方法 BMC，区别是 BMC 不抽象、靠 SAT 暴力展开 k 步
hoare-logic —— 谓词逻辑做”程序对不对”的另一条路线，证明导向 vs 枚举导向

反向链接

biere-bmc-1999 —— Bounded Model Checking — 把硬件验证翻译成一道 SAT 题
clarke-cegar-2003 —— CEGAR — 用反例自动改进抽象，让大软件能被验证
cousot-abstract-interpretation —— Cousot 抽象解释 — 给静态分析一套统一数学框架
hoare-logic —— Hoare Logic — 把”程序对不对”变成”数学证明对不对”
sagiv-shape-analysis —— Sagiv 参数化形状分析 — 用三值逻辑证明链表树仍是链表树
slam-microsoft —— SLAM — 让 Windows 驱动 bug 自己撞到工具上