Semantics-Guided Synthesis
summary
Framework that takes a grammar, a big‑step semantics expressed as Constrained Horn Clauses, and examples or formulas as specs, then reduces synthesis to CHC proof search solved by Z3/Spacer. Implements MESSY and synthesizes 12 realizable benchmarks while proving 178 benchmarks unrealizable (66 via standard semantics); it is the first method reported to prove unrealizability for imperative programs with unbounded loops by encoding syntax+semantics as CHCs and extracting programs from proof trees.
AI-written summary · about
chapters (6)
- 0:00Introduction
- 0:44SemanticsGuided Synthesis
- 3:17SemanticsGuided Synthesis Framework
- 22:00Messi
- 23:41Results
- 26:41Proof
related talks
18mVerifying Solutions to Semantics-Guided Synthesis Problems
21mSynthesizing Formal Semantics from Executable Interpreters
15mVerifying and Improving Halide’s Term Rewriting System with Program Synthesis
20mAutomating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…)
18mAutomated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic(…)
22mCounterexample-Guided Inference of Modular Specifications
38mConstrained Horn Clauses Satisfiability via Catamorphic Abstractions
31mLetting users do the undecidable: lessons from program synthesis