Efficient Bottom-Up Synthesis for Programs with Local Variables
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 JanDisplayed time zone: London change
10:30 - 11:50 | |||
10:30 20mTalk | Implementation and Synthesis of Math Library FunctionsDistinguished Paper POPL | ||
10:50 20mTalk | Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations POPL | ||
11:10 20mTalk | 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 20mTalk | Optimal Program Synthesis via Abstract Interpretation POPL Stephen Mell University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Osbert Bastani University of Pennsylvania |