Big Ideas in Program Synthesis
summary
Survey of program synthesis highlights three concrete tactics and working tools: observational equivalence prunes enumerative search by keeping one representative per example-driven equivalence class; counterexample-guided inductive synthesis (CEGIS) combines an inductive enumerator with a verifier—Sketch synthesizes (~x) & (x+1) for the least-significant-zero mask and proves it for 32-bit vectors; deductive synthesis uses separation-logic proofs to drive search—SuSLig synthesizes an in-place tree-to-doubly-linked-list routine after ~6,000 proof nodes. Snippy integrates bottom-up synthesis into VS Code with live projection boxes and it works.
AI-written summary · about
chapters (4)
- 0:00Introduction to synthesis
- 1:43Observational equivalence
- 24:42Counter-example guided synthesis
- 37:47Deductive synthesis
related talks
38mProgram Synthesis: A Dream Realized?
29mSyntia: Synthesizing the Semantics of Obfuscated Code
16mJust-in-Time Learning for Bottom-Up Enumerative Synthesis
01h 10mNeurosymbolic Program Synthesis: Bridging Perception and Reasoning in Real-World(…)
40mType-Driven Program Synthesis
17mExplainable Program Synthesis by Localizing Specifications
16mFeedback-Driven Semi-supervised Synthesis of Program Transformations
25mInductive Synthesis of Structurally Recursive Functional Programs from Non-recur...