Counterexample-Guided Inference of Modular Specifications

Explore a 28-minute lecture on counterexample-guided inference of modular specifications presented by Bill Hallahan from Binghamton University at the Simons Institute. Delve into the world of modular verification tools and their role in allowing programmers to compositionally specify and prove function specifications. Discover a novel counterexample-guided algorithm designed to automatically infer specifications for functions called within a target function. Examine the algorithm's parameterization over a verifier, counterexample generator, and constraint-guided synthesizer, and understand how the soundness and completeness of these components contribute to the overall algorithm's effectiveness. Learn about additional requirements that extend the completeness result to an infinite set of possible specifications. Conclude by reviewing an evaluation of this technique across various benchmarks, gaining insights into its practical applications in the field of synthesis of models and systems.