PLDI 2025
Mon 16 - Fri 20 June 2025 Seoul, South Korea

This program is tentative and subject to change.

Wed 18 Jun 2025 11:10 - 11:30 at Grand Ball Room 2 - Synthesis Chair(s): Sébastien Bardin

There are many state-of-the-art techniques for loop bound analysis. Most of them target an upper bound for a given program, and others find a lower bound. \emph{Exact} bound analysis still remains largely unexplored, but it offers new applications. To compute an \emph{exact} bound for a program it is necessary to reason about the possible values the program's inputs can take and how they relate to each other. Since inputs can vary on any given execution of the program, it makes the problem of computing an exact bound challenging. In this work, we present a new approach to find an exact bound by way of \emph{precondition synthesis} which iteratively considers under-approximations of a program under which the bound can be precomputed over initial values of program variables. For each precondition, our approach synthesizes a function over program variables such that when the function is applied to the initial values of the program variables, its output is an exact bound for the program. We reduce the precondition synthesis problem to that of \emph{safety verification} which lends its correctness guarantees to the exact bounds we compute. {Our technique has been implemented in a tool called \textsc{Elba}, and we show that it is effective on a set of challenging single loop benchmarks under Linear Integer Arithmetic.}

This program is tentative and subject to change.

Wed 18 Jun

Displayed time zone: Seoul change

10:30 - 12:10
SynthesisPLDI Research Papers at Grand Ball Room 2
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