Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification

The paper presents what it describes as the first contract-based regression verification tool. LLMs infer partial contracts from the checker’s counterexamples, without a separate specification phase, and assume-guarantee reasoning verifies program flow. On Frama-C-Problems, caller-sufficient contracts were usually already as tight as strengthened contracts. On the third-party EqBench-C suite, the checker produced zero false equivalence proofs and identified nine program pairs that EqBench reportedly mislabels as equivalent. Experiments also cover the ANSSI X509 parser and compare verification rates with AutoSpec and Preguss.