Spring 2021

Counterexample Guided Inference of Modular Specifications

Monday, Apr. 5, 2021 10:00 am10:30 am

Add to Calendar


Bill Hallahan (Yale University)



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.

PDF icon Slides239.94 KB