反例引导的抽象精化 CEGAR

形式陈述

闭环的四个阶段

CEGAR 维护具体系统 $C$ 、选定抽象域及当前抽象模型 $A_i$ 。每轮执行：构造或更新抽象；对 $A_i$ 做模型检查；若得到抽象反例则检查具体可行性；若不可行，利用失败原因生成更精细的 $A_{i+1}$ 。

可靠抽象要求

Beh(C)\subseteq\gamma(Beh(A_i)).

因此抽象系统证明安全即可推出具体安全。抽象系统发现反例却只说明“可能违反”，必须经过 concretization feasibility check。

精化应满足行为收缩

\gamma(Beh(A_{i+1})) \subseteq \gamma(Beh(A_i)),

并排除当前伪反例。只增加新术语而不删除该路径，不构成有效精化进展。

用谓词立方体定义每一条抽象边

以下固定数学整数变量 $x,y$ ，没有溢出。按谓词抽象选择有限谓词表 $P=(p_1,\ldots,p_m)$ ；一个位向量 $b\in\{0,1\}^m$ 对应立方体

C_b(x,y)=\bigwedge_{j=1}^m \begin{cases}p_j(x,y),&b_j=1,\\\neg p_j(x,y),&b_j=0.\end{cases}

只保留可满足立方体，控制位置 $pc$ 单独保存。每个具体状态恰好落入一个立方体。对具体转移 $T_e$ ，抽象边的定义是

(pc,b)\xrightarrow e(pc',b') \quad\Longleftrightarrow\quad \exists x,y,x',y'.\ C_b(x,y)\land T_e(pc,x,y,pc',x',y')\land C_{b'}(x',y').

初始节点另由 $I\land C_b$ 可满足定义；求边时不添加初始约束，否则会把尚未由分析发现、却可能在后续出现的状态错误删掉。终端错误位置统一合并为一个 bad 节点，只问能否到达它。

这一定义的可靠性有直接证明：把任一具体初态映射到其立方体，得到抽象初态；每次具体转移的实际端点就是存在量词的见证，所以归纳把整条具体运行映为抽象运行。因而抽象图无 bad 路径就证明具体安全。反过来，每条抽象边的见证可以不同，不保证能拼成一条具体路径。[1, §2]

直觉

在循环头保留状态，而不是混淆语句中间点

考虑程序

text

x := 0
y := 0
while nondet:
    x := x + 1
    y := y + 1
assert x == y

取循环头 $h$ 、断言检查点 $c$ 和错误终点 bad。把一次完整循环体的两条赋值合成为 $h$ 到 $h$ 的一条转移；这两个控制点之间没有其他分支或断言，所以这种摘要保持本例的错误可达性。顺序执行到 x++ 后、y++ 前确实有 $x=y+1$ ，不能声称 $x=y$ 在每一个语句中间点都保持。

省略不再影响错误可达性的成功终止节点，模型是

\begin{aligned} I&:\ pc=h\land x=0\land y=0,\\ T_{\mathrm{loop}}&:\ pc=h\land pc'=h\land x'=x+1\land y'=y+1,\\ T_{\mathrm{exit}}&:\ pc=h\land pc'=c\land x'=x\land y'=y,\\ T_{\mathrm{fail}}&:\ pc=c\land pc'=\mathsf{bad}\land x\ne y \land x'=x\land y'=y. \end{aligned}

循环可以任意继续或退出；证明目标是所有能够退出的运行都通过断言，而不是强迫非确定循环终止。bad 没有后继。下文把循环边、退出边、失败边分别列完，不依赖隐藏的转移规则。

粗谓词 $P_0=(x\ge0,y\ge0)$ 把 $(1,1)$ 与 $(1,2)$ 都放进 $11$ 。前者是从初态执行一轮后的实际状态，后者却能触发断言失败。抽象图允许在这个合并节点把前缀见证与失败见证连接，伪反例由此产生。增加关系谓词 $x=y$ 才能区分二者。

粗抽象的11节点把真实前缀与失败见证连接；加入相等谓词后，可达111节点只有安全自环和退出，错误边留在不可达的不等分支。 — 谓词精化删除伪路径

例子与边界

粗图的全部转移

$P_0$ 的四个立方体均非空。下面给出所有循环边；同一行未列出的目标全部不可满足，第三列按目标顺序给出源状态，执行 $(x,y)\mapsto(x+1,y+1)$ 就得到相应目标见证。

源位向量	循环目标	对应源状态见证
$00$	$00,01,10,11$	$(-2,-2),(-2,-1),(-1,-2),(-1,-1)$
$01$	$01,11$	$(-2,0),(-1,0)$
$10$	$10,11$	$(0,-2),(0,-1)$
$11$	$11$	$(0,0)$

未列边要求一个非负坐标经加一后成为负数，所以不存在。退出边恰是每个 $(h,b)\to(c,b)$ ，因为两个变量不变。四个检查节点都存在失败边： $00,01,10,11$ 的见证分别可取 $(-1,-2),(-1,0),(0,-1),(0,1)$ 。这就列全了图，而不只是可达部分。

唯一初始位向量是 $11$ ，因此粗图可达集合为

R_0=\{(h,11),(c,11),\mathsf{bad}\}.

其中 $(h,11)$ 有循环自环、通向 $(c,11)$ 的退出边，而检查点有通向 bad 的失败边。

同一条路径的公式为何 UNSAT

选择“循环一次，再退出并失败”的抽象反例。给各位置引入不同状态帧，得到

\begin{aligned} \Phi={}&x_0=0\land y_0=0\\ &\land x_1=x_0+1\land y_1=y_0+1\\ &\land x_2=x_1\land y_2=y_1\land x_2\ne y_2. \end{aligned}

三个 $11$ 立方体的非负约束在此被等式蕴涵，可加上而不改变结果。最后的失败边恒等地进入错误终点，已消去其不再使用的末帧。等式强迫 $x_1=y_1=x_2=y_2=1$ ，与 $x_2\ne y_2$ 矛盾，故 $\Phi$ 不可满足。

失败边本身可以用 $(1,2)$ 作见证，但这个状态接不上前缀强迫的 $(1,1)$ 。因此检查每条边分别可满足，不能代替整条路径检查。即使模型检查器选择零轮循环的更短反例，同样会被 $x_0=y_0=0$ 排除；此处选择一轮是为了显式展示转移帧。

一般地，若反例指定了抽象节点 $b_0,\ldots,b_k$ 及动作 $e_0,\ldots,e_{k-1}$ ，应检查

I(s_0)\land\bigwedge_{i=0}^k C_{b_i}(s_i) \land\bigwedge_{i=0}^{k-1}T_{e_i}(s_i,s_{i+1})\land Bad(s_k).

合并的 bad 节点取 $C_{\mathsf{bad}}=\top$ 。若只指定动作序列而不指定立方体，则可以省略中间立方体条件；两种查询不能混用。SAT 的同一个模型给出可重放具体路径，UNSAT 才证明这条抽象路径是伪的。反例轨迹必须保存这些帧之间的关联。[1, §4.2]

插值给出相等谓词

在循环后切开 $\Phi$ ，令

\begin{aligned} A&=(x_0=0\land y_0=0\land x_1=x_0+1\land y_1=y_0+1),\\ B&=(x_2=x_1\land y_2=y_1\land x_2\ne y_2). \end{aligned}

二者共享的自由符号只有 $x_1,y_1$ 。选择

J(x_1,y_1)\equiv x_1=y_1.

$A\Rightarrow J$ ，因为双方都等于一； $J\land B$ 不可满足，因为退出保持相等。 $J$ 只含共享符号，因此满足 Craig 插值的三项条件。它不是唯一插值，也不是断言任意求解器都会返回这个式子。把帧下标去掉，就得到可在程序位置使用的新谓词 $x=y$ 。[2, §3；3, §5.1]

精图的全部转移与最终可达集

加入 $x=y$ ，按 $P_1=(x\ge0,y\ge0,x=y)$ 排列三个位。可满足立方体为

000,001,010,100,110,111.

$011$ 与 $101$ 不存在：相等整数不可能具有相反的非负性。所有循环边如下，同样按目标顺序列源见证。

源位向量	循环目标	对应源状态见证
$000$	$000,010,100$	$(-3,-2),(-2,-1),(-1,-2)$
$001$	$001,111$	$(-2,-2),(-1,-1)$
$010$	$010,110$	$(-2,0),(-1,0)$
$100$	$100,110$	$(0,-2),(0,-1)$
$110$	$110$	$(0,1)$
$111$	$111$	$(0,0)$

没有列出的目标都不可满足：两个符号位只会从0变1，等号位由 $x'-y'=x-y$ 保持。还需检查粗符号条件未排除的 $000\to110$ ；两个负整数若同时加一变为非负，只能都从 $-1$ 出发，这与源的“不相等”位矛盾，故也没有该边。这说明不能把两个非负谓词独立处理后随意组合转移。

每个可满足立方体都保留恒等退出边。只有等号位为0的 $000,010,100,110$ 有失败边，它们可分别用 $(-1,-2),(-1,0),(0,-1),(0,1)$ 作见证。等号位为1的 $001,111$ 与失败 guard 不相容，没有失败边。新的唯一初态是 $(h,111)$ ，所以

R_1=\{(h,111),(c,111)\},\qquad\mathsf{bad}\notin R_1.

丢弃第三位把每个精节点映回粗节点；任一精边的具体见证也是对应粗边的见证，因此精图没有增加具体行为。原先用相等前缀接不等失败见证的路径被删除，而任何真实运行仍由存在转移定义覆盖。

收敛与失败边界

有限状态系统若精化策略最终能区分每个必要具体状态，最坏可退化到精确模型并终止。对无限状态软件，CEGAR 不保证找到有限谓词集，也可能不断产生新反例而不收敛。

求解器 unknown 既不是真实反例也不是不可行证明。把超时当 UNSAT 会错误删除可能真实路径，把它当 SAT 又可能报告无法重放的警报；工具应保留 unknown 状态。

精化也可能过拟合一条路径：加入只排除某个具体常数的谓词，下一轮出现同构伪反例。好的概括来自失败原因，而非反例表面数字。

推论与应用

安全结论的三个可检查义务

最终证书可以只交出上面的谓词表、完整边判定依据以及集合 $R_1$ ，检查器验证三点：初态包含于 $R_1$ ； $R_1$ 对每条抽象后继封闭； $R_1$ 不含 bad。第一点由零初值，第二点由 $111$ 的唯一循环目标与恒等退出，第三点由等号位与失败 guard 冲突得到。结合形式部分的运行映射归纳，就证明原程序任意多轮后的退出都安全。

也可把相同证书写成循环头和检查点的归纳断言

x\ge0\land y\ge0\land x=y.

初值满足它；两个坐标同时加一保持它；退出不改变它；它蕴涵断言 $x=y$ 。这四个有限义务覆盖无限多个可能的迭代次数，不需要为每次迭代分别枚举轨迹。

若把循环体改为 x:=x+1; y:=y+2，同一轮后的实际状态是 $(1,2)$ ，原路径公式变成SAT，模型给出真实反例；此时不能继续用 $x=y$ 精化来删掉它。精化的职责是排除抽象制造的行为，而不是排除程序确实能够执行的错误。

与抽象解释的关系

抽象解释提供可靠 over-approximation 的数学基础；CEGAR 是选择和迭代改进抽象的一种控制循环。它不是独立于 soundness 的“反复跑模型检查”技巧。

区间阈值、谓词集合、状态分裂和 transition refinement 都可成为 refinement 维度。每种选择要说明哪部分 concretization 变小以及为何仍覆盖具体行为。

终止时还应区分两种证书：真实反例附具体可行路径；安全结果附最终抽象的可靠性和抽象模型无反例证明。只保存“循环若干轮后工具返回 safe”不足以复核结论。

参考资料

[1] Edmund Clarke、Orna Grumberg、Somesh Jha、Yuan Lu、Helmut Veith，Counterexample-guided Abstraction Refinement，CAV 2000，154–169页；§2给出存在抽象与安全性蕴涵，§4.2讨论同一具体路径的可行性及累计像集检查。本文的整数循环图与可靠性在正文独立给出。

[2] Kenneth L. McMillan，Interpolation and SAT-Based Model Checking，CAV 2003，1–13页；第1页定义插值三条件，§3说明路径切分时共享符号是切口状态。该文的主要算法是有限状态插值模型检查。

[3] Thomas A. Henzinger、Ranjit Jhala、Rupak Majumdar、Kenneth L. McMillan，Abstractions from Proofs，POPL 2004，232–244页；§2与§4定义谓词抽象，§§4–5.1用带状态帧的路径公式、插值切分和谓词清理连接不可行证明与精化。

形式陈述 ​

闭环的四个阶段 ​

用谓词立方体定义每一条抽象边 ​

在循环头保留状态，而不是混淆语句中间点 ​

粗图的全部转移 ​

同一条路径的公式为何 UNSAT ​

插值给出相等谓词 ​

精图的全部转移与最终可达集 ​

收敛与失败边界 ​

安全结论的三个可检查义务 ​

与抽象解释的关系 ​

反向链接