Bottom-Up Synthesis of Recursive Functional Programs using Angelic Execution
summary
The paper presents a bottom-up synthesis method that actually builds recursive functional programs by executing incomplete programs under angelic semantics, extracts the assumptions those angelic executions make, strengthens the specification, and retries; the implementation Burst uses version space learning to make many incremental synthesis calls cheap and relies on CDCL-style minimal assumption cores to reduce backtracking. Evaluation on prior benchmarks times out at two minutes on a laptop and solves 94% of the benchmarks, outperforming prior work; current support restricts recursion to the top level and excludes mutual recursion.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 0:39What is BottomUp Synthesis
- 3:00TopDown vs BottomUp
- 3:58Example
- 6:37Contributions
- 7:29Key difficulty
- 7:53Angelic Execution
- 8:12Angelic Recursion
- 9:45HighLevel Algorithm
- 11:37Recap
- 12:16Get Assumptions
- 15:36Theoretical guarantees
- 15:48Benchmarks
- 17:00Comparison with Burst
- 17:30Related Work
- 18:05Conclusion
related talks
17mEfficient Bottom-Up Synthesis for Programs with Local Variables
25mRecursive Program Synthesis using Paramorphisms
20mOptimal Program Synthesis via Abstract Interpretation
31mLetting users do the undecidable: lessons from program synthesis
15mProducts of Recursive Programs for Hypersafety Verification
01h 05mControl Flow Obfuscation for Featherweight Java + Efficient Fair Conjunction
20mAutomating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…)
26mProgram Synthesis Using Example Propagation