Abstract
Modular verification tools, such as Dafny and LiquidHaskell, 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. Further, we describe a SyGuS based approach to building the constraint guided synthesizer. We conclude with an evaluation demonstrating our technique on a variety of benchmarks.