一句话：提出反例引导算法，自动推断模块化验证所需的被调函数规约，并在有限与大小受限无限规约空间下给出可靠完备性结果。
模块化验证工具要求程序员为被调函数手动编写规约，才能组合式证明目标函数规约，这构成使用门槛。本文提出一种反例引导的规约推断算法，自动为被调函数合成所需规约；算法以验证器、反例生成器和约束引导合成器为参数，若三者在有限候选规约集上可靠且完备，则整体算法可靠且完备。作者进一步提出大小受限的合成函数，将完备性推广到无限规约集，并针对线性整数算术约束给出具体合成方法。最后在多种基准上评估该技术。
Modular verification tools allow programmers to compositionally specify and prove function specifications. When using a modular verifier, proving a specification about a function f requires additional specifications for the functions called by f . With existing state of the art tools, programmers must manually write the specifications for callee functions. We present a counterexample guided algorithm to automatically infer these specifications. The algorithm is parameterized over a verifier, counterexample generator, and constraint guided synthesizer. We show that if each of these three components is sound and complete over a finite set of possible specifications, our algorithm is sound and complete as well. Additionally, we introduce size-bounded synthesis functions, which extends our completeness result to an infinite set of possible specifications. In particular, we describe a size-bounded synthesis function for linear integer arithmetic constraints. We conclude with an evaluation demonstrating our technique on a variety of benchmarks.
@article{paperbot3155,
title = {Counterexample-Guided Inference of Modular Specifications},
author = {William T. Hallahan and Ranjit Jhala and Ruzica Piskac},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720505}
}