Parameterized Infinite-State Reactive Synthesis
summary
A counterexample‑guided loop synthesizes a single parameterized infinite‑state reactive program and a proof by: (1) enumerating small concrete parameter instances and synthesizing implementations, (2) anti‑unification to find shared structure, (3) filling holes with syntax‑guided synthesis expressions, and (4) checking invariants and ranking functions with an SMT backend. Prototype uses CBC5 and C3, solves most benchmarks the authors add, produces counterexample parameters when verification fails, and admits undecidability so it may not terminate for some specs.
AI-written summary · about
chapters (16)
- 0:00Parameterized reactive synthesis
- 1:05Reactive systems and specs
- 3:55Robot and environment example
- 5:21Environment assumptions in specs
- 6:24First strategy from spec
- 8:11Why parameterized synthesis
- 9:15Key observations for synthesis
- 9:57Generating programs and certificates
- 11:22Generalizing strategies
- 13:29Anti-unification and syntax-guided synthesis
- 14:54Refining candidate program
- 16:23Role of invariants and ranking
- 17:48Ranking functions with assumptions
- 19:14Synthesis procedure summary
- 20:18Tool implementation and benchmarks
- 21:25Q&A
related talks
24mSynthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications
19mSolving Infinite-State Games via Acceleration
15mProducts of Recursive Programs for Hypersafety Verification
29mRewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata
31mParameterized Verification of Systems with Precise (0,1)-Counter Abstraction
21mMechanizing the CMP Abstraction for Parameterized Verification
11mFinding Invariants of Distributed Systems: It's a Small (Enough) World After All
21mMonotone Procedure Summarization via Vector Addition Systems and Inductive Potentials