Can Reactive Synthesis and Syntax-Guided Synthesis Be Friends?
summary
Combines SyGuS for data-heavy fragments with temporal stream logic (TSL) reactive synthesis for control: SyGuS synthesizes pure functions (e.g., add1 then add1 for 0→2) as ASTs, each AST level is turned into a timestep using the TSL next operator, producing assumptions that weaken guarantees; the combined TSL+assumptions feeds a reactive synthesizer to produce automata or executable C/JS. Implements Linux CFS scheduler and a music synthesizer from specs, uses linear integer arithmetic, works on provided benchmarks though some timing-generalization limits remain.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 0:30SyntaxGuided
- 1:12Reactive Synthesis
- 1:55The Catch
- 2:38Linux Scheduler
- 3:32Simple Scheduler
- 4:16Temporal Stream Logic
- 4:52Data Section
- 5:37Synthesis Problem
- 6:09Key Idea
- 6:46General Overview
- 8:54Synthesis
- 9:47Transformation
- 11:48Combining
- 14:06Benchmarks
- 14:17Summary
related talks
21mSynthesizing Formal Semantics from Executable Interpreters
31mLetting users do the undecidable: lessons from program synthesis
19mEnhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipu...
18mVerifying Solutions to Semantics-Guided Synthesis Problems
26mProgram Synthesis Using Example Propagation
30mSemantics-Guided Synthesis
28mSynthesizing Abstract Transformers
20mOptimal Program Synthesis via Abstract Interpretation