SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Thu 21 Oct 2021 13:50 - 14:05 at Zurich B - Program Synthesis Chair(s): Kedar Namjoshi
Thu 21 Oct 2021 21:50 - 22:05 at Zurich B - Program Synthesis - mirror Chair(s): Hakjoo Oh

The generalizability of PBE solvers is the key to the empirical synthesis performance. Despite the importance of generalizability, related studies on PBE solvers are still limited. In theory, few existing solvers provide theoretical guarantees on generalizability, and in practice, there is a lack of PBE solvers with satisfactory generalizability on important domains such as conditional linear integer arithmetic (CLIA). In this paper, we adopt a concept from the computational learning theory, Occam learning, and perform a comprehensive study on the framework of synthesis through unification (STUN), a state-of-the-art framework for synthesizing programs with nested if-then-else operators. We prove that Eusolver, a state-of-the-art STUN solver, does not satisfy the condition of Occam learning, and then we design a novel STUN solver, PolyGen, of which the generalizability is theoretically guaranteed by Occam learning. We evaluate PolyGen on the domains of CLIA and demonstrate that PolyGen significantly outperforms two state-of-the-art PBE solvers on CLIA, Eusolver and Euphony, on both generalizability and efficiency.

Thu 21 Oct

Displayed time zone: Central Time (US & Canada) change

13:50 - 15:10
Program SynthesisOOPSLA at Zurich B +8h
Chair(s): Kedar Namjoshi Nokia Bell Labs
13:50
15m
Talk
Generalizable Synthesis through UnificationVirtual
OOPSLA
Ruyi Ji Peking University, Jingtao Xia Peking University, Yingfei Xiong Peking University, Zhenjiang Hu Peking University
DOI
14:05
15m
Talk
Gauss: Program Synthesis by Reasoning over GraphsVirtual
OOPSLA
Rohan Bavishi University of California at Berkeley, Caroline Lemieux Microsoft Research, Koushik Sen University of California at Berkeley, Ion Stoica University of California at Berkeley
DOI
14:20
15m
Talk
APIfix: Output-Oriented Program Synthesis for Combating Breaking Changes in LibrariesVirtual
OOPSLA
Xiang Gao National University of Singapore, Arjun Radhakrishna Microsoft, Gustavo Soares Microsoft, Ridwan Salihin Shariffdeen National University of Singapore, Sumit Gulwani Microsoft, Abhik Roychoudhury National University of Singapore
DOI
14:35
15m
Talk
LooPy: Interactive Program Synthesis with Control StructuresVirtual
OOPSLA
Kasra Ferdowsi University of California at San Diego, Shraddha Barke University of California at San Diego, Hila Peleg Technion, Sorin Lerner University of California at San Diego, Nadia Polikarpova University of California at San Diego
DOI
14:50
20m
Live Q&A
Discussion, Questions and Answers
OOPSLA

21:50 - 23:10
Program Synthesis - mirrorOOPSLA at Zurich B
Chair(s): Hakjoo Oh Korea University
21:50
15m
Talk
Generalizable Synthesis through UnificationVirtual
OOPSLA
Ruyi Ji Peking University, Jingtao Xia Peking University, Yingfei Xiong Peking University, Zhenjiang Hu Peking University
DOI
22:05
15m
Talk
Gauss: Program Synthesis by Reasoning over GraphsVirtual
OOPSLA
Rohan Bavishi University of California at Berkeley, Caroline Lemieux Microsoft Research, Koushik Sen University of California at Berkeley, Ion Stoica University of California at Berkeley
DOI
22:20
15m
Talk
APIfix: Output-Oriented Program Synthesis for Combating Breaking Changes in LibrariesVirtual
OOPSLA
Xiang Gao National University of Singapore, Arjun Radhakrishna Microsoft, Gustavo Soares Microsoft, Ridwan Salihin Shariffdeen National University of Singapore, Sumit Gulwani Microsoft, Abhik Roychoudhury National University of Singapore
DOI
22:35
15m
Talk
LooPy: Interactive Program Synthesis with Control StructuresVirtual
OOPSLA
Kasra Ferdowsi University of California at San Diego, Shraddha Barke University of California at San Diego, Hila Peleg Technion, Sorin Lerner University of California at San Diego, Nadia Polikarpova University of California at San Diego
DOI
22:50
20m
Live Q&A
Discussion, Questions and Answers
OOPSLA