PLDI 2025
Mon 16 - Fri 20 June 2025 Seoul, South Korea
Wed 18 Jun 2025 10:30 - 10:50 at Orchid - Synthesis Chair(s): Sébastien Bardin

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 Jun

Displayed 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
20m
Talk
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
20m
Talk
A Concurrent Approach to String Transformation Synthesis
PLDI Research Papers
Yuantian Ding Purdue University, Xiaokang Qiu Purdue University
DOI
11:10
20m
Talk
Exact Loop Bound Analysis
PLDI Research Papers
Daniel Riley Florida State University, Grigory Fedyukovich Florida State University
DOI
11:30
20m
Talk
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
20m
Talk
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