Fri 21 Jan 2022 17:05 - 17:30 at Salon III - Synthesis Chair(s): Paul Downen

We present a novel bottom-up method for the synthesis of functional recursive programs. While bottom-up synthesis techniques can work better than top-down methods in certain settings, there is no prior technique for synthesizing recursive programs from logical specifications in a purely bottom-up fashion. The main challenge is that effective bottom-up methods need to execute sub-expressions of the code being synthesized, but it is impossible to execute a recursive subexpression of a program that has not been fully constructed yet. In this paper, we address this challenge using the concept of angelic semantics. Specifically, our method finds a program that satisfies the specification under angelic semantics (we refer to this as angelic synthesis), analyzes the assumptions made during its angelic execution, uses this analysis to strengthen the specification, and finally reattempts synthesis with the strengthened specification. Our proposed angelic synthesis algorithm is based on version space learning and therefore deals effectively with many incremental synthesis calls made during the overall algorithm. We have implemented this approach in a prototype called Burst and evaluate it on synthesis problems from prior work. Our experiments show that Burst is able to synthesize a solution to 95% of the benchmarks in our benchmark suite, outperforming prior work.

Fri 21 Jan

Displayed time zone: Eastern Time (US & Canada) change

16:40 - 17:30
SynthesisPOPL at Salon III
Chair(s): Paul Downen University of Massachusetts Lowell
16:40
25m
Research paper
Learning Formulas in Finite Variable LogicsDistinguished PaperInPerson
POPL
Paul Krogmeier University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign
DOI Media Attached
17:05
25m
Research paper
Bottom-Up Synthesis of Recursive Functional Programs using Angelic ExecutionDistinguished PaperRemote
POPL
Anders Miltner University of Texas at Austin, Adrian Trejo Nuñez University of Texas at Austin, Ana Brendel University of Texas at Austin, Swarat Chaudhuri University of Texas at Austin, Isil Dillig University of Texas at Austin
DOI Media Attached