部分契约已足够：基于大模型推断的可靠回归验证

论文提出首个基于契约的回归验证工具，用大模型从反例自动推断调用者所需的部分契约，再通过 assume-guarantee 推理验证程序流。作者在 Frama-C-Problems、ANSSI X509 parser 与 EqBench-C 上报告：部分契约通常已接近最紧契约，EqBench-C 上零误报等价证明，并发现九组被 EqBench 错标为等价的程序对。