论文技术总结：基于测试库契约的验证 (Verification Modulo Tested Library Contracts)

1. 问题背景与定义

核心问题：
在大规模软件系统的形式化验证中，完全自动化面临巨大挑战。传统的模块化验证要求为大型库（Library）编写强契约（Contracts）并对其进行形式化证明，这通常难以实现。然而，客户端（Client）程序通常较小，且其逻辑依赖于库的行为。

VMTLC 问题定义：
本文提出了“基于测试库契约的验证”（Verification Modulo Tested Library Contracts, VMTLC）问题。其目标是在不形式化验证库代码的前提下，自动合成库方法的契约，使得：

1. 客户端正确性：假设库满足这些合成契约，客户端程序的形式化验证（如断言检查）能够成功。
2. 契约通过测试：这些合成契约必须能够通过给定的确定性测试生成器（Test Generator）的严格测试，即测试器无法找到违反契约的测试用例。

两种契约形式：

• 模块化契约 (Modular Contracts)：库方法在所有可能的状态和输入下都必须满足契约。测试器独立地对库方法进行测试。
• 上下文契约 (Contextual Contracts)：这是本文提出的新概念。契约仅需在客户端程序的特定调用上下文中成立。即，库方法仅在客户端实际调用的状态和参数下满足契约。这种契约通常比模块化契约更简单、更容易合成，因为它们利用了客户端对库的隐式约束（例如，客户端只向集合插入正数，那么契约可以简化为“移除的元素总是正数”，而无需处理负数情况）。

2. 方法论与框架

作者提出了一种**反例引导的归纳学习（Counterexample-Guided Inductive Synthesis, CEGIS）**框架，名为 Dualis。该框架通过迭代循环协同工作，同时合成客户端的归纳不变式（Inductive Invariants）和库方法的契约。

核心组件

1. 约束求解器 (Constraint Solver)：
   • 将验证条件转化为约束霍恩子句 (Constrained Horn Clauses, CHCs)。
   • 输入包括客户端的 CHC 约束和来自测试器的正样本（Positive Examples）。
2. 泛化 CHC 求解器 (Generalizing CHC Solver)：
   • 这是框架的关键。普通的 CHC 求解器可能会“过拟合”测试样本（即契约仅覆盖已知的正样本，导致无法泛化）。
   • 本文采用 ICE 学习算法 (Implication Counterexample Learning) 来实现泛化求解。ICE 求解器利用正样本、负样本和蕴含反例来学习归纳不变式和契约，倾向于寻找最简逻辑表达式，从而实现泛化。
   • 实现了三种 ICE 学习器：
     • HornICE：基于决策树学习。
     • LLM：利用大语言模型（如 Gemini）生成候选契约和不变式。
     • HornICE+LLM：结合两者，利用 LLM 生成原子谓词，再由 HornICE 构建决策树。
3. 测试生成器 (Test Generator)：
   • 使用模糊测试框架（AFL++）作为测试引擎。
   • 模块化模式：独立构造库对象并调用库方法，检查契约是否被违反。
   • 上下文模式：直接运行客户端程序，监控库方法在客户端上下文中的调用，检查契约是否被违反。
   • 如果测试失败，提取违反契约的输入作为正样本反馈给求解器。

工作流程

1. 初始化：生成客户端的 CHC 约束，初始正样本集为空。
2. 合成循环：
   • ICE 求解器尝试合成满足 CHC 约束且包含当前正样本的契约和不变式。
   • 测试器对合成结果进行验证。
   • 若测试通过：验证成功，终止。
   • 若测试失败：提取反例（正样本），加入样本集，返回步骤 2 重新合成（要求新契约覆盖新样本）。

3. 关键贡献

1. VMTLC 问题形式化：首次形式化定义了结合形式化验证（客户端）与测试（库）的验证问题，并提出了上下文契约这一新范式，显著降低了合成难度。
2. 通用学习框架：提出了一种通用的反例引导学习框架，能够同时处理客户端不变式合成和库契约合成，并支持多种 ICE 学习算法（包括符号方法和 LLM）。
3. 泛化求解器设计：强调了在 VMTLC 场景下，CHC 求解器必须具备泛化能力（Generalization），避免过拟合测试样本，这是解决该问题的理论核心。
4. 工具实现 (Dualis)：开发了名为 Dualis 的工具，集成了 Z3 求解器、AFL++ 模糊测试器以及多种 ICE 学习器（HornICE, LLM, 混合模式）。
5. 实证评估：在 43 个基于真实开源库（如 Folly, Abseil）的基准测试上进行了评估，证明了该方法在现有自动化验证工具（如 SeaHorn）失效的情况下依然有效。

4. 实验结果

• 基准测试：使用了 43 个 C++ 客户端程序，涉及从 100 到 3000 行代码的库。这些基准测试大多无法被现有的全自动验证工具（如 SeaHorn）验证。
• 求解成功率：
  • 模块化契约：纯 LLM 方法解决了 38/43 个基准，HornICE+LLM 解决了 25 个，纯 HornICE 解决了 19 个。
  • 上下文契约：表现更优，纯 LLM 解决了 41/43 个，HornICE+LLM 解决了 28 个，HornICE 解决了 21 个。
  • 结论：上下文契约不仅更容易合成，而且成功率显著高于模块化契约。
• LLM 的作用：LLM 在生成复杂的逻辑谓词方面表现出色，特别是在 HornICE 的模板受限时。混合方法（LLM 提供原子公式 + HornICE 构建结构）在效率和成功率之间取得了良好平衡。
• 有效性验证：
  • 人工审查和逻辑蕴含检查表明，所有合成的契约在逻辑上是正确的。
  • 额外的 30 分钟模糊测试未发现任何违反合成契约的情况。
  • 突变测试 (Mutant Study)：在 30 个故意引入的、难以被测试发现的错误程序中，VMTLC（模块化）成功拒绝了所有错误程序；而 VMTLC（上下文）合成了 11 个虚假契约（Spurious Contracts）导致验证通过。这表明上下文契约虽然更易合成，但存在合成虚假契约的风险，不过在实际中这种概率较低。

5. 意义与局限性

意义：

• 可扩展性：为大规模代码库的自动化验证提供了新路径。通过放弃对库的完全形式化验证（改为测试），换取了客户端验证的自动化和可扩展性。
• 实用性：上下文契约的概念非常符合实际开发场景，利用客户端的特定使用模式简化了规范，使得自动合成成为可能。
• 技术融合：成功将形式化方法（CHC, ICE）、模糊测试和大语言模型（LLM）有机结合，展示了混合智能在程序验证中的潜力。

局限性与未来工作：

• 虚假契约风险：特别是上下文契约，如果测试覆盖不全，可能会合成出能通过测试但逻辑错误的契约，从而错误地“证明”了有缺陷的客户端。
• 观察者方法限制：当前方法依赖库提供的观察者方法（Observer Methods）。如果库缺乏足够的观察者方法（如无法获取链表最后一个元素），则难以合成有效契约。
• 堆内存推理：目前主要处理封装良好的对象，对于涉及共享堆指针修改的复杂场景，契约语言需要更丰富（如分离逻辑）。

总结：
这篇论文提出了一种务实且创新的验证范式，通过“验证客户端 + 测试库契约”的混合策略，结合先进的归纳学习和 LLM 技术，成功解决了传统自动化验证难以处理的大规模库依赖问题。其提出的上下文契约概念和 Dualis 工具为未来的程序验证研究提供了重要的方向。