Generalized Program Sketching by Abstract Interpretation and Logical Abduction
summary
Defines a generalized sketching problem and implements a working prototype synthesizer for C that fills holes with arbitrary arithmetic or boolean expressions, not just constants. It combines forward and backward abstract interpretation (uses the polyhedra domain) to get premises and sufficient postconditions, then solves abduction queries with the EXPLAIN abduction solver (and MyAL/SMT) to produce the weakest concrete expressions that prove assertions. Evaluation on numerical linear-arithmetic benchmarks succeeds on several examples and runs faster than Sketch and FamilySketcher, but it is limited to domains and theories the abduction solver supports.
AI-written summary · about
chapters (11)
- 0:00Program sketching intro
- 1:11Generalized sketching problem
- 3:02Abstract interpretation for sketches
- 7:52Contributions and formal problem
- 11:50Abduction problem and solution
- 13:14Single-hole synthesis algorithm
- 14:41Implementation and tools
- 15:43Comparison with tools
- 17:30Tool performance and limits
- 19:19Conclusion and future work
- 20:02Q&A