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 OctDisplayed time zone: Central Time (US & Canada) change
13:50 - 15:10 | |||
13:50 15mTalk | Generalizable Synthesis through UnificationVirtual OOPSLA Ruyi Ji Peking University, Jingtao Xia Peking University, Yingfei Xiong Peking University, Zhenjiang Hu Peking University DOI | ||
14:05 15mTalk | 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 15mTalk | 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 15mTalk | 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 20mLive Q&A | Discussion, Questions and Answers OOPSLA |
21:50 - 23:10 | |||
21:50 15mTalk | Generalizable Synthesis through UnificationVirtual OOPSLA Ruyi Ji Peking University, Jingtao Xia Peking University, Yingfei Xiong Peking University, Zhenjiang Hu Peking University DOI | ||
22:05 15mTalk | 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 15mTalk | 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 15mTalk | 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 20mLive Q&A | Discussion, Questions and Answers OOPSLA |