Program Synthesis for Artifacts beyond Programs
summary
Three synthesis projects convert non‑regular artifacts into regular program synthesis problems and actually build working tools: a first‑order theorem prover called Gambit synthesizes memory fences and atomic sections under relaxed models, runs on >100 race benchmarks and finds fixes in about one second each; a semantic‑action synthesizer generates attribute‑grammar actions for parsers and a Java interpreter and reproduces examples from a SPIN case study; and a CEGIS‑style pipeline synthesizes abstract transformers with simultaneous soundness and precision checks for five string and three numeric domains, matching manual runtimes.
AI-written summary · about
chapters (7)
- 0:00Program synthesis beyond programs
- 1:03Regular programs and constructs
- 2:30Concurrent programs with fences
- 7:47Semantic actions for parsing
- 10:45Abstract transformers for domains
- 14:21Future directions
- 14:47Q&A
related talks
21mProgram Synthesis From Partial Traces
01h 05mVerifying Infinitely Many Programs at Once
19mSynthesizing Specifications
15mHieraSynth: A Parallel Framework for Complete Super-Optimization with Hierarchical(…)
14mSynthesizing Contracts Correct Modulo a Test Generator
52mThink Abstractly, Work Concretely
15mAutomatic Synthesis of Data-Flow Analyzers
13mMetamorph: Synthesizing Large Objects from Dafny Specifications