Bi-directional reduced-product abstract interpretation is a key technology for inductive program synthesis. I will present our recent approach to example-based program synthesis via forward-and-backward abstract interpretations that effectively reduce the gigantic search space of programs. The forward abstract interpretation computes possible outputs of a program given inputs, while the backward abstract interpretation computes possible inputs of a program’s given outputs. By iteratively performing the two abstract interpretations for incomplete programs, we can determine in advance if any completion of each partial program can satisfy the given input-output examples. Our experiment results for synthesizing bit-manipulation programs (such as code in Hacker’s Delight) show that our approach significantly outperforms the state-of-the-art approaches thanks to the sophisticated abstract interpretation techniques. Joint work with Yongho Yoon and Woosuk Lee, presented at PLDI 2023.

Professor