Inductive Program Synthesis via Iterative Forward-Backward Abstract Interpretation
A key challenge in example-based program synthesis is the gigantic search space of programs. To address this challenge, various work proposed to use abstract interpretation to prune the search space. However, most of existing approaches have focused only on forward abstract interpretation, and thus cannot fully exploit the power of abstract interpretation. In this paper, we propose a novel approach to inductive program synthesis via iterative forward-backward abstract interpretation. The forward abstract interpretation computes possible outputs of a program given inputs, while the backward abstract interpretation computes possible inputs of a program given outputs. By iteratively performing the two abstract interpretations in an alternating fashion, we can effectively determine if any completion of each partial program as a candidate can satisfy the input-output examples. We apply our approach to a standard formulation, syntax-guided synthesis (SyGuS), thereby supporting a wide range of inductive synthesis tasks. We have implemented our approach and evaluated it on a set of benchmarks from the prior work. The experimental results show that our approach significantly outperforms the state-of-the-art approaches thanks to the sophisticated abstract interpretation techniques.
Tue 20 JunDisplayed time zone: Eastern Time (US & Canada) change
09:00 - 11:00 | |||
09:00 20mTalk | Trace-Guided Inductive Synthesis of Recursive Functional ProgramsDistinguished Paper PLDI Research Papers DOI | ||
09:20 20mTalk | Inductive Program Synthesis via Iterative Forward-Backward Abstract Interpretation PLDI Research Papers Yongho Yoon Seoul National University, Woosuk Lee Hanyang University, Kwangkeun Yi Seoul National University DOI | ||
09:40 20mTalk | ImageEye: Batch Image Processing using Program Synthesis PLDI Research Papers Celeste Barnaby University of Texas at Austin, Jocelyn (Qiaochu) Chen University of Texas at Austin, Roopsha Samanta Purdue University, Işıl Dillig University of Texas at Austin DOI | ||
10:00 20mTalk | One Pixel Adversarial Attacks via Sketched Programs PLDI Research Papers DOI | ||
10:20 20mTalk | Absynthe: Abstract Interpretation-Guided Synthesis PLDI Research Papers Sankha Narayan Guria University of Maryland, Jeffrey S. Foster Tufts University, David Van Horn University of Maryland DOI Pre-print | ||
10:40 20mTalk | Conflict-Driven Synthesis for Layout Engines PLDI Research Papers Junrui Liu University of California, Santa Barbara, Yanju Chen University of California at Santa Barbara, Eric Atkinson MIT, Yu Feng University of California at Santa Barbara, Rastislav Bodík Google Research, Brain Team DOI |