部分契约就足够了：可靠的、由大语言模型推断的回归验证
Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification
浏览论文内容
中文总结 AI 辅助
研究软件回归验证难题，提出基于契约的工具，探讨部分契约的充分性，通过强化契约、自动推断等方法，实现可靠验证，在多方面取得良好效果，证明安全保留条件等价性。
中文摘要 AI 辅助
软件持续演进，确保补丁保留预期行为而无需重新验证整个代码库仍然困难。回归验证解决此问题，但现有技术需要昂贵的全程序推理或依赖实际中很少可用的手动编写规范。我们提出首个基于契约的回归验证工具。通过证明所有函数版本匹配行为来确保契约可靠性，然后通过假设-保证来验证程序流。我们探讨部分的、调用者足够的契约而非完整行为规范是否足够。在Frama-C-Problems上，我们强化每个推断契约使其超出调用者需求并衡量其收紧程度。结果表明调用者足够的契约几乎已达到最紧，部分规范契约捕获了几乎所有可达到的紧密度。底层的回归检查是可靠的，在第三方EqBench-C套件上从未编造等价性，还发现了EqBench误标记为等价的九对。契约本身从检查器自己的反例自动推断，无需单独的规范步骤，在Frama-C-Problems和ANSSI X509解析器上达到与AutoSpec和Preguss工具相当的验证率，通过结果证明至少具有同样强的属性，即安全保留条件等价性：强制执行加调用者足够性。
英文摘要
Software evolves continuously, yet ensuring that a patch preserves intended behavior without re-verifying an entire codebase remains difficult. Regression verification addresses this problem, but existing techniques require expensive whole-program reasoning or rely on manually written specifications that are rarely available in practice. We present the first contract-based regression verification tool. Contract soundness is ensured by proving all function versions match the behavior. The contract then verifies program flow via assume-guarantee. We ask whether a partial, caller-sufficient contract, rather than a full behavioral specification, is enough. On Frama-C-Problems we strengthen each inferred contract past what the caller needs and measure how much tighter it becomes. It barely moves: for most targets in every model the caller-sufficient contract is already the tightest the loop reaches, and our tightness comparator rates the partial and strengthened contracts equivalent for the large majority of targets it can compare. Partial-spec contracts thus capture nearly all the attainable tightness, so stopping at caller-sufficiency costs almost nothing. The regression check underneath is sound: on the third-party EqBench-C suite it never fabricates an equivalence, returning zero false proofs and reporting an unprovable difference instead. It also surfaced nine pairs that EqBench mislabels as equivalent, more than a concurrent tool reports. The contracts themselves are inferred automatically from the checker's own counterexamples, with no separate specification step; on Frama-C-Problems and the ANSSI X509 parser this reaches a verification rate comparable to tools AutoSpec and Preguss, while a passing result certifies at least as strong a property, which we call \emph{safety-preserving conditional equivalence}: enforcement plus caller-sufficiency.
发表机构
- The University of Manchester（曼彻斯特大学）
机构由 AI 辅助整理，请以论文原文为准。
