Automating Unrealizability Logic: Hoare-style Proof Synthesis for Infinite Sets of(…)
summary
Presents Wuldo, the first implementation of an Unrealizability Logic (UL) proof synthesizer that decouples a fixed proof skeleton from parametric nonterminal summaries, producing Hoare-style proofs over grammars that denote infinite sets of programs. Wuldo checks or synthesizes summaries, handles specifications that require infinite counterexamples or arbitrary Hoare triples, reuses summaries across queries, and speeds verification 1.96× versus proving summaries from scratch. Benchmarks show it proves cases out of reach for prior solvers; synthesis sometimes fails when summaries need complex existentials.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 2:12Running example and grammar
- 3:36Limitations of solvers
- 4:39Unrealizability logic
- 5:22Induction and summaries
- 7:51Proof structure insight
- 11:41Proof synthesis algorithm
- 12:01Benchmark results
- 14:28Challenges with summaries
- 15:32Conclusion
related talks
27mUnrealizability Logic
01h 05mVerifying Infinitely Many Programs at Once
23mSeparating the Wheat from the Chaff: Understanding (In-)Completeness of Proof(…)
52mThink Abstractly, Work Concretely
19mProof Automation for Linearizability in Separation Logic
14mSynthesizing Implication Lemmas for Interactive Theorem Proving
14mSynthesizing Contracts Correct Modulo a Test Generator
20mOn Extending Incorrectness Logic with Backwards Reasoning