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

Syntax-guided synthesis (SyGuS) aims to find a program satisfying semantic specification as well as user-provided structural hypotheses. There are two main synthesis approaches: enumerative synthesis, which repeatedly enumerates possible candidate programs and checks their correctness, and deductive synthesis, which leverages a symbolic procedure to construct implementations from specifications. Neither approach is strictly better than the other: automated deductive synthesis is usually very efficient but only works for special grammars or applications; enumerative synthesis is very generally applicable but limited in scalability.

In this paper, we propose a cooperative synthesis technique for SyGuS problems with the conditional linear integer arithmetic (CLIA) background theory, as a novel integration of the two approaches, combining the best of the two worlds. The technique exploits several novel divide-and-conquer strategies to split a large synthesis problem to smaller subproblems. The subproblems are solved separately and their solutions are combined to form a final solution. The technique integrates two synthesis engines: a pure deductive component that can efficiently solve some problems, and a height-based enumeration algorithm that can handle arbitrary grammar. We implemented the cooperative synthesis technique, and evaluated it on a wide range of benchmarks. Experiments showed that our technique can solve many challenging synthesis problems not possible before, and tends to be more scalable than state-of-the-art synthesis algorithms.

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

08:00 - 09:00
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
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
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