Counterexample-Guided Inference of Modular Specifications

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. We present a counterexample guided algorithm to automatically infer these specifications. The algorithm is parameterized over a verifier, counterexample generator, and constraint guided synthesizer. 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 additional requirements which extend our completeness result to an infinite set of possible specifications. We conclude with an evaluation demonstrating our technique on a variety of benchmarks.