POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Wed 17 Jan 2024 11:10 - 11:30 at Kelvin Lecture - Synthesis 1 Chair(s): Soham Chakraborty

We propose a new synthesis algorithm that can efficiently search programs with local variables (e.g., those introduced by lambdas). Prior bottom-up synthesis algorithms are not able to evaluate programs with free local variables, and therefore cannot effectively reduce the search space of such programs (e.g., using standard observational equivalence reduction techniques), making synthesis slow. Our algorithm can reduce the space of programs with local variables. The key idea, dubbed lifted interpretation, is to lift up the program interpretation process, from evaluating one program at a time to simultaneously evaluating all programs from a grammar. Lifted interpretation provides a mechanism to systematically enumerate all binding contexts for local variables, thereby enabling us to evaluate and reduce the space of programs with local variables. Our ideas are instantiated in the domain of web automation. The resulting tool, Arborist, can automate a significantly broader range of challenging tasks more efficiently than state-of-the-art techniques including WebRobot and Helena.

Wed 17 Jan

Displayed time zone: London change

10:30 - 11:50
Synthesis 1POPL at Kelvin Lecture
Chair(s): Soham Chakraborty TU Delft
10:30
20m
Talk
Implementation and Synthesis of Math Library FunctionsDistinguished Paper
POPL
Ian Briggs University of Utah, Yash Lad University of Utah, Pavel Panchekha University of Utah
10:50
20m
Talk
Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations
POPL
Yuantian Ding Purdue University, Xiaokang Qiu Purdue University
11:10
20m
Talk
Efficient Bottom-Up Synthesis for Programs with Local Variables
POPL
Xiang Li University of Michigan, Ann Arbor, Xiangyu Zhou University of Michigan, Rui Dong University of Michigan, Yihong Zhang University of Washington, Xinyu Wang University of Michigan
Pre-print
11:30
20m
Talk
Optimal Program Synthesis via Abstract Interpretation
POPL
Stephen Mell University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Osbert Bastani University of Pennsylvania