Presynthesis: Towards Scaling Up Program Synthesis with Finer-Grained Abstract Semantics
summary
Proposes offline presynthesis that builds a semantics tree automaton and a reachability oracle so online synthesis reduces to fast graph reachability queries; implements the idea in Foresighter and evaluates on string, matrix and SQL benchmarks. Offline build produces graphs of about 500,000 nodes and 500 million edges, taking ~7 hours plus ~5 hours to index and producing ~51 GB offline graph. Results show Foresighter outperforms prior tools and keeps improving as abstraction granularity increases, avoiding the online U‑shaped slowdown.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:24Problem setup
- 3:10Finer-grained abstractions
- 4:36Offline precomputation
- 6:01Search as graph building
- 7:48Semantics database
- 9:55Bidirectional reachability
- 10:59Online efficiency
- 11:20Evaluation domains
- 12:42Performance impact
- 13:24Conclusion
- 13:45Q&A
related talks
20mOptimal Program Synthesis via Abstract Interpretation
20mAutomating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…)
20mSemantic foundations of potential-synthesis for expected amortised-cost analysis
14mDataflow-Based Pruning for Speeding up Superoptimization
31mLetting users do the undecidable: lessons from program synthesis
15mHieraSynth: A Parallel Framework for Complete Super-Optimization with Hierarchical(…)
17mEfficient Bottom-Up Synthesis for Programs with Local Variables
21mSynthesizing Formal Semantics from Executable Interpreters