Verifying Solutions to Semantics-Guided Synthesis Problems
summary
Framework reduces SemGuS verification to reduction to µCLP and classifies problems into SMT-encodable, CHC-encodable, and µCLP-encodable cases, implements verifiers for each encoding, and plugs them into an enumeration-based synthesizer. Evaluation shows the virtual-best verifier solves 709 of 730 queries; integration with an enumerator synthesized 135 problems, of which 74 were previously unsolvable by existing SemGuS tools. Proposed SemGuS extension adds reactive/nondeterministic expressiveness; current tool scales to small programs.
AI-written summary · about
chapters (13)
- 0:00Semantic guided synthesis intro
- 1:04Synthesis problems examples
- 2:27Framework requirements
- 4:10Verifying synthesized programs
- 5:17Non-recursive programs with SMT
- 7:03Recursive programs with CHC solvers
- 9:11Total correctness with MuSLP
- 12:04Closing verifier-synthesizer loop
- 12:25Extending SIGUIS to reactive
- 13:30Evaluation benchmarks
- 14:55Solver performance comparison
- 15:17Integration with enumeration
- 16:02Q&A
related talks
30mSemantics-Guided Synthesis
21mSynthesizing Formal Semantics from Executable Interpreters
19mEnhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipu...
31mLetting users do the undecidable: lessons from program synthesis
20mAutomating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…)
15mVerifying and Improving Halide’s Term Rewriting System with Program Synthesis
22mCounterexample-Guided Inference of Modular Specifications
30mAnalyzing Programs with SMT Solvers