基于 SMT 的软件验证

路径条件的符号轨迹 ​

程序

assume x >= 0
y := x + 1
assert y > 0

产生反例公式

在线性整数算术中 UNSAT，因此断言成立。若 x,y 是固定宽度无符号位向量，最大值加一回绕到零，公式可能 SAT；把机器值错建模为无界整数会漏掉真实错误。

求解器模型还需映射回源变量和路径。一个 SAT 赋值若违反前端未编码的语言规则，只是编码反例，不是程序反例。

模型中的未解释函数只受 congruence 约束：相同输入给相同输出，不具备单调、纯函数以外的领域性质。把库函数编码为 uninterpreted 可以保守保留多种返回，却无法证明依赖其算术语义的性质；若同时遗漏副作用，则可能不再保守。

对浮点，IEEE NaN、符号零和舍入模式需用 floating-point theory 或已证明近似。把浮点比较改成实数比较会错误使用全序和结合律。

分支、SSA 与 phi ​

符号执行沿分支积累 path condition；static single assignment 给每次赋值新版本，使等式无歧义。汇合处用 $ite$ 或 phi 连接分支值：

符号执行理路符号执行Symbolic execution · Classical symbolic execution用输入符号、变量表达式和路径条件逐步执行程序，完整分叉并重放反例，区分覆盖证明、有限界和unknown。将这一接口展开为位置、变量表达式和路径条件三元状态，手算三条终端路径并重放输入(1,2)。混合执行理路混合执行Concolic execution · Concolic testing · Dynamic symbolic execution · 动态符号执行沿具体运行同步积累符号条件，翻转路径前缀并求新输入重放，说明覆盖保证依赖精确建模、完整调度和查询结果。再从(0,0)的实际运行出发，翻转路径前缀而丢弃旧后缀，逐轮生成覆盖另外两条路径的输入；精确小域枚举与SMT后端的范围分别声明。

若只把两边约束合取，会错误要求同一次执行同时走两条互斥路径；若只取析取而不关联输出版本，又会允许值来自错误分支。

路径枚举可能指数增长。合并公式、bounded unrolling、抽象与 lemma 学习用于控制规模，但都需保持路径条件语义。

堆内存常编码成数组 $Mem:Addr\to Val$。store/select 公理能表示读写，但 allocation freshness、对象边界与类型有效性仍需额外约束。若任意整数都可作地址，求解器会找到现实内存模型不允许的别名。

SSA 版本化还应覆盖 heap：每次写产生 $Me{m}_{i+1}=store(Me{m}_i,a,v)$。继续从旧 $Me{m}_i$ 读取会在验证公式中“撤销”写入，产生假证明。

循环与不变式 ​

有限展开只能验证给定迭代界。全局循环证明需要候选不变式 $Inv$，并产生初始化、保持和退出三类义务：

SMT 可检查候选，不自动保证能发现足够强的不变式。template、abstract interpretation、Houdini 或 interpolation 可生成候选，各有完备边界。

Houdini不变式推断理路Houdini 不变式推断Houdini invariant inference · Houdini algorithm从有限谓词候选中反复剔除初始化或保持失败项，输出可独立复核的归纳合取，并证明候选语言内的最大性。给出有限候选表内的执行闭环：以初始化或保持反例剔除候选，因前提变弱重新检查，最终交出归纳合取。其五状态例逐轮删除p0、p1、p2，保留p3、p4；候选合取最大性与推出安全目标是分别核验的两项结论。

终止还需 variant 的良基下降义务；只证明 invariant 是 partial correctness。

函数递归类似循环：contract 作为归纳假设用于递归调用，同时要证明函数体在假设下实现 contract。若递归调用不满足前置，或 termination measure 未下降，不能因调用摘要已知就跳过。

invariant 推断产生的候选可能只在采样路径上成立。交给 SMT 检查初始化和保持，正是把候选升级为证明的关键；若保持失败，模型给出的是归纳反例，不一定是从程序初态可达的真实 bug。

理论组合与 unknown ​

SMT 理论有各自可判定片段。非线性整数算术、量词、递归函数和浮点混合可能返回 unknown 或超时。unknown 不是 UNSAT，不能当作证明成功。

数组 extensionality、指针别名和内存对象生命周期需精确编码。把两指针默认不同可让证明轻易通过，却排除了真实 alias 行为。

量词通常依赖 instantiation trigger。trigger 太弱会超时，太窄会漏掉所需实例而返回 unknown；若求解器仍返回 SAT/UNSAT，其语义保证应独立于启发式，但某些不完备理论组合只承诺 unknown。工具不能把“没有生成反例实例”当作全称量词已证。

非线性实算术与非线性整数算术性质不同；前者有特定判定程序，后者很快触及不可判定性。把 solver 对某组公式的成功经验写成片段完备性需要正式依据。

求解器内部 bug 也属于可信计算基。proof-producing solver 可导出可检查证明，但理论证明格式覆盖度和独立 checker 仍需说明。

模块摘要与边界 ​

函数调用可用 contract 摘要：调用者证明前置，随后假设后置和 frame condition。摘要漏写全局副作用会让所有调用证明不可靠。

外部库、并发内存模型、未定义行为和编译器转换都需要独立接口。SMT 只判断收到的逻辑公式，不验证公式是否完整表达实际软件。

并发程序若逐线程生成 VC，需 rely–guarantee、权限或原子性证明连接线程干扰。假设其他线程不改共享变量相当于加入错误 frame condition，单线程 SMT 证明不会自动扩展到并发执行。

证书保存应包含 SMT-LIB 输入、求解器版本、选项和结果；随机种子或预处理变化可能影响性能，但已检查 proof certificate 才能缩小对具体二进制的信任。