Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Fri 19 Jun 2020 08:00 - 08:20 at PLDI Research Papers live stream - Synthesis III Chair(s): Santosh Nagarakatte

We consider the problem of automatically establishing that a given syntax-guided-synthesis (SyGuS) problem is unrealizable (i.e., has no solution). We formulate the problem of proving that a SyGuS problem is unrealizable over a finite set of examples as one of solving a set of equations: the solution yields an overapproximation of the set of possible outputs that any term in the search space can produce on the given examples. If none of the possible outputs agrees with all of the examples, our technique has proven that the given SyGuS problem is unrealizable. We then present an algorithm for exactly solving the set of equations that result from SyGuS problems over linear integer arithmetic (LIA) and LIA with conditionals (CLIA), thereby showing that LIA and CLIA SyGuS problems over finitely many examples are decidable. We implement the proposed technique and algorithms in a tool called Nay. Nay can prove unrealizability for 70/132 existing SyGuS benchmarks, with running times comparable to those of the state-of-the-art tool Nope. Moreover, Nay can solve 11 benchmarks that Nope cannot solve.

Fri 19 Jun
Times are displayed in time zone: Pacific Time (US & Canada) change

08:00 - 09:00: Synthesis III PLDI Research Papers at PLDI Research Papers live stream
Chair(s): Santosh NagarakatteRutgers University, USA

YouTube lightning session video

08:00 - 08:20
Exact and Approximate Methods for Proving Unrealizability of Syntax-Guided Synthesis Problems
PLDI Research Papers
Qinheping HuUniversity of Wisconsin-Madison, USA, John CyphertUniversity of Wisconsin-Madison, USA, Loris D'AntoniUniversity of Wisconsin-Madison, USA, Thomas RepsUniversity of Wisconsin-Madison, USA
08:20 - 08:40
Question Selection for Interactive Program Synthesis
PLDI Research Papers
Ruyi JiPeking University, China, Jingjing LiangPeking University, China, Yingfei XiongPeking University, China, Lu ZhangPeking University, China, Zhenjiang HuPeking University, China
08:40 - 09:00
Reconciling Enumerative and Deductive Program Synthesis
PLDI Research Papers
Kangjing HuangPurdue University, USA, Xiaokang QiuPurdue University, USA, Peiyuan ShenPurdue University, USA, Yanjun WangPurdue University, USA