When a program synthesis task starts from an ambiguous specification, the synthesis process often involves an iterative specification refinement process. We introduce the Programming by Navigation Synthesis Problem, a new synthesis problem adapted specifically for supporting iterative specification refinement in order to find a particular target solution. In contrast to prior work, we prove that synthesizers that solve the Programming by Navigation Synthesis Problem show all valid next steps (Strong Completeness) and only valid next steps (Strong Soundness). To meet the demands of the Programming by Navigation Synthesis Problem, we introduce an algorithm to turn a type inhabitation oracle (in the style of classical logic) into a fully constructive program synthesizer. We then define such an oracle via sound compilation to Datalog. Our empirical evaluation shows that this technique results in an efficient Programming by Navigation synthesizer that solves tasks that are either impossible or too large for baselines to solve. Our synthesizer is the first to guarantee that its specification refinement process satisfies both Strong Completeness and Strong Soundness.
Wed 18 JunDisplayed time zone: Seoul change
10:30 - 12:10 | SynthesisPLDI Research Papers at Orchid Chair(s): Sébastien Bardin CEA LIST, University Paris-Saclay | ||
10:30 20mTalk | Programming by Navigation PLDI Research Papers Justin Lubin University of California at Berkeley, Parker Ziegler University of California at Berkeley, Sarah E. Chasins University of California at Berkeley DOI Pre-print | ||
10:50 20mTalk | A Concurrent Approach to String Transformation Synthesis PLDI Research Papers DOI | ||
11:10 20mTalk | Exact Loop Bound Analysis PLDI Research Papers DOI | ||
11:30 20mTalk | Multi-stage Relational Programming PLDI Research Papers Michael Ballantyne Northeastern University, Rafaello Sanna Harvard University, Jason Hemann Seton Hall University, William E. Byrd University of Alabama at Birmingham, Nada Amin Harvard University DOI | ||
11:50 20mTalk | Program Synthesis From Partial Traces PLDI Research Papers Margarida Ferreira Carnegie Mellon University; INESC-ID; Instituto Superior Técnico - University of Lisbon, Victor Nicolet Amazon, Joey Dodds Amazon, Daniel Kroening Amazon DOI |