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 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:30 - 19:00 | |||
18:30 10mTalk | Generating Collection Transformations from Proofs POPL Link to publication DOI | ||
18:40 10mTalk | 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 10mTalk | Combining the Top-down Propagation and Bottom-up Enumeration for Inductive Program Synthesis POPL Woosuk Lee Hanyang University, South Korea Link to publication DOI |