POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Thu 15 Jan 2026 16:35 - 17:00 at Dortoirs - Synthesis 2 Chair(s): Marco Campion

We propose a method to synthesize a parameterized infinite-state system that can be instantiated for different parameter values. The specification is given in a parameterized temporal logic that allows for data variables as well as parameters that encode properties of the environment. Our synthesis method runs in a counterexample-guided loop consisting of four steps: (1) we synthesize concrete systems for some small parameter instantiations using existing techniques. (2) We generalize the concrete systems into a parameterized program. (3) We create a proof candidate consisting of an invariant and a ranking function. (4) We check the proof candidate for consistency with the program. If the proof succeeds, the parameterized program is valid. Otherwise, we identify a parameter value for which it fails and add a new concrete instance to step one. To generalize programs and create proof candidates, we use a combination of anti-unification and syntax-guided synthesis to express the differences between the programs as a function of the parameters. We evaluate our approach on new examples and examples from the literature that are manually parameterized.

Thu 15 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

16:10 - 17:00
Synthesis 2POPL at Dortoirs
Chair(s): Marco Campion Inria Paris - ENS - Université PSL
16:10
25m
Talk
Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers
POPL
Xuanyu Peng University of California at San Diego, Dominic Kennedy University of Utah, Yuyou Fan University of Utah, Ben Greenman University of Utah, USA, John Regehr University of Utah, Loris D'Antoni University of California at San Diego
DOI
16:35
25m
Talk
Parameterized Infinite-State Reactive Synthesis
POPL
Benedikt Maderbacher Graz University of Technology, Roderick Bloem Graz University of Technology
DOI