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
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:30 - 19:00: SynthesisPOPL at POPL-A
18:30 - 18:40
Talk
Generating Collection Transformations from Proofs
POPL
Michael BenediktUniversity of Oxford, UK, Pierre PradicOxford University
Link to publication DOI
18:40 - 18:50
Talk
Semantics-Guided Synthesis
POPL
Jinwoo KimUniversity of Wisconsin-Madison, Qinheping HuUniversity of Wisconsin-Madison, USA, Loris D'AntoniUniversity of Wisconsin-Madison, USA, Thomas RepsUniversity of Wisconsin--Madison
Link to publication DOI
18:50 - 19:00
Talk
Combining the Top-down Propagation and Bottom-up Enumeration for Inductive Program Synthesis
POPL
Woosuk LeeHanyang University, South Korea
Link to publication DOI