Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Fri 22 Jan 2021 18:40 - 18:50 at POPL-A - Synthesis

This paper develops a new framework for program synthesis, called semantics-guided synthesis (SemGuS), that allows a user to provide both the syntax and the semantics for the constructs in the language. SemGuS accepts a recursively defined big-step semantics, which allows it, for example, to be used to specify and solve synthesis problems over an imperative programming language that may contain loops with unbounded behavior. The customizable nature of SemGuS also allows synthesis problems to be defined over a non-standard semantics, such as an abstract semantics. In addition to the SemGuSframework, we develop an algorithm for solving SemGuS problems that is capable of both synthesizing programs and proving unrealizability, by encoding a SemGuS problem as a proof search over Constrained Horn Clauses: in particular, our approach is the first that we are aware of that can prove unrealizabilty for synthesis problems that involve imperative programs with unbounded loops, over an infinite syntactic search space. We implemented the technique in a tool called MESSY, and applied it to both SyGuS problems (i.e., over expressions) and synthesis problems over an imperative programming language.

Fri 22 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:30 - 19:00
SynthesisPOPL at POPL-A
18:30
10m
Talk
Generating Collection Transformations from Proofs
POPL
Michael Benedikt University of Oxford, UK, Pierre Pradic Oxford University
Link to publication DOI
18:40
10m
Talk
Semantics-Guided Synthesis
POPL
Jinwoo Kim University of Wisconsin-Madison, Qinheping Hu University of Wisconsin-Madison, USA, Loris D'Antoni University of Wisconsin-Madison, USA, Thomas Reps University of Wisconsin--Madison
Link to publication DOI
18:50
10m
Talk
Combining the Top-down Propagation and Bottom-up Enumeration for Inductive Program Synthesis
POPL
Woosuk Lee Hanyang University, South Korea
Link to publication DOI