Counterexample-Guided Inference of Modular Specifications
summary
A counterexample-guided algorithm automatically infers missing callee specifications so a modular verifier can prove a client function, parameterized by a verifier, counterexample generator, and constraint-guided synthesizer and proven sound and complete over finite spec sets. A SMT-based LEA synthesizer generates linear integer arithmetic refinements, and size-bounded synthesis extends completeness to infinite candidate spaces. Evaluation on Liquid Haskell and case studies (including K-means with ~34 helper functions) shows it finds adequate specs and verifies benchmarks, with most cost in symbolic execution and occasional slow synthesis.
AI-written summary · about
chapters (9)
- 0:00Modular specification verification
- 4:39Modular verifiers' limitations
- 8:08Abstract counterexamples in chains
- 9:32Counterexample-guided synthesis
- 13:02Soundness and completeness
- 14:49LEA with SMT solvers
- 16:33Performance benchmarks
- 17:16K-means case study
- 18:41Q&A
related talks
27mCompiling higher-order specifications to SMT solvers: how to deal with rejection ...
14mLOUD: Synthesizing Strongest and Weakest Specifications
31mLetting users do the undecidable: lessons from program synthesis
35mThe Mastermind behind Refinement Types
28mImplicit modules, a middle step towards modular implicits
30mSemantics-Guided Synthesis
31mFormal Specification
30mAnalyzing Programs with SMT Solvers