Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification
2026-07-11 • Software Engineering
Software EngineeringArtificial Intelligence
AI summaryⓘ
The authors developed a new tool that helps check if software patches keep the program's behavior consistent without re-checking everything. Instead of needing full detailed rules for every function, their tool uses partial contracts focused on what callers need, which is usually enough. Their method automatically infers these contracts and proved to be very reliable and efficient on several benchmarks. It also caught some mistakes in existing test suites where programs were wrongly marked as equivalent. Overall, their approach offers a practical way to verify software updates safely with less effort.
regression verificationsoftware patchfunction contractcaller-sufficient contractFrama-Cassume-guarantee reasoningconditional equivalencecounterexample-guided inferenceprogram verificationsafety properties
Authors
Yiannis Charalambous, Rafael Menezes, Youcheng Sun, Lucas C. Cordeiro
Abstract
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.