基于 SMT 的软件验证

验证条件接口 ​

给定前置条件 $P$、程序 $C$ 与后置条件 $Q$，最弱前置条件公理库最弱前置条件Weakest precondition保证程序建立给定后置条件的最弱状态谓词。生成 $wp(C,Q)$。Hoare 义务可化为

再查询其否定

是否为可满足公式公理库可满足公式Satisfiable formula存在至少一个真值赋值使其为真的命题公式。。UNSAT 证明当前语义和理论下不存在违反输入；SAT 模型给出候选反例状态。

SMT 在布尔 SAT 上加入整数、实数、位向量、数组、未解释函数等理论。选择哪个理论属于程序语义，不只是求解器性能选项。

验证条件生成器必须证明自己的规则与语言语义对应。对顺序组合，它按逆序传递后置；对分支，它在 guard 下分别生成义务；对过程调用，它使用 callee contract 并建立 frame condition。漏掉一种语句或把异常路径当正常返回，会在公式进入求解器之前破坏可靠性。

可把 VC 作为 proof obligation 列表而非一个大合取，便于定位失败；但共享假设必须复制或由增量上下文维护，不能因拆分丢失全局 invariant。

路径条件的符号轨迹 ​

程序

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 连接分支值：

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

路径枚举可能指数增长。合并公式、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 可生成候选，各有完备边界。

终止还需 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 才能缩小对具体二进制的信任。