Unrealizability Logic
summary
A Hoare-style proof system called unrealizability logic gives checkable proofs that a synthesis search space has no solution, overapproximating infinite sets of programs with unrealizability triples and composing by grammar structure. It handles per-program counterexamples by vectorized inputs, proves the XOR-without-NOT case via an oddness invariant over all expressions, uses strongest-postcondition-style rules and structural induction, and demonstrates practical uses: certifying optimality, pruning symbolic-execution paths, and guiding top-down synthesis.
AI-written summary · about
chapters (11)
- 0:00Intro
- 1:43Program Synthesis in a Nutshell
- 6:02Dealing with Sets of Programs: Unrealizability Triples
- 7:43Connecting Unrealizability with Unrealizability Triples
- 8:46Using Unrealizability Triples: Inference Rules
- 10:47Proofs in Unrealizability Logic: Deriving Invariants
- 15:25Synchronizing Between Inputs: Vectorized Semantics
- 17:56Synchronization on Multiple Vector-States
- 18:57Motivations for Unrealizability: Optimization
- 19:56Using Unrealizability Logic: Symbolic Execution
- 20:14Motivations for Unrealizability: Synthesis
related talks
20mAutomating Unrealizability Logic: Hoare-style Proof Synthesis for Infinite Sets of(…)
01h 05mVerifying Infinitely Many Programs at Once
52mThink Abstractly, Work Concretely
22mExecution Time Program Verification With Tight Bounds
23mSpecifying and Verifying Future Conditions
20mOn Extending Incorrectness Logic with Backwards Reasoning
13mEncode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
14mA Hoare Logic For Symmetry Properties