Synthesizing Specifications
summary
Algorithm synthesizes all best L-properties that are sound, precise (no strictly more precise L-property exists), and complete (no further L-properties can tighten the conjunction). It combines an example-driven synthesizer, a check-sound verifier and a novel check-precision loop that freezes safe negative examples to resolve conflicts. Implementation Spyro uses SKETCH for synthesis plus an external verifier to prove soundness; on 35 benchmarks 23 properties are proven automatically, it finds algebraic specs and even exposes a hashmap bug.
AI-written summary · about
chapters (9)
- 0:00Specification synthesis intro
- 1:10Problem definition
- 2:55Key contributions
- 5:04Running example
- 6:31Conflicting negative examples
- 8:40Applications and results
- 11:53Case studies
- 13:19Summary
- 14:26Q&A
related talks
22mProgram Synthesis for Artifacts beyond Programs
21mProgram Synthesis From Partial Traces
27mUnrealizability Logic
14mSynthesizing Contracts Correct Modulo a Test Generator
23mSpecifying and Verifying Future Conditions
20mAutomating Unrealizability Logic: Hoare-style Proof Synthesis for Infinite Sets of(…)
14mSynthesizing Implication Lemmas for Interactive Theorem Proving
01h 05mVerifying Infinitely Many Programs at Once