In this paper, we propose an automated approach to finding correct and efficient memoization algorithms from a given declarative specification. This problem has two major challenges: (i) a memoization algorithm is too large to be handled by conventional program synthesizers; (ii) we need to guarantee the efficiency of the memoization algorithm. To address this challenge, we structure the synthesis of memoization algorithms by introducing the local objective function and the memoization partition function and reduce the synthesis task to two smaller independent program synthesis tasks. Moreover, the number of distinct outputs of the function synthesized in the second synthesis task also decides the efficiency of the synthesized memoization algorithm, and we only need to minimize the number of different output values of the synthesized function. However, the generated synthesis task is still too complex for existing synthesizers. Thus, we propose a novel synthesis algorithm that combines the deductive and inductive methods to solve these tasks. To evaluate our algorithm, we collect 42 real-world benchmarks from Leetcode, the National Olympiad in Informatics in Provinces-Junior (a national-wide algorithmic programming contest in China), and previous approaches. Our approach successfully synhesizes 39/42 problems in a reasonable time, outperforming the baselines.
Wed 25 OctDisplayed time zone: Lisbon change
14:00 - 15:30 | |||
14:00 18mTalk | Mobius: Synthesizing Relational Queries with Recursive and Invented Predicates OOPSLA Aalok Thakkar University of Pennsylvania, Nathaniel Sands University of Southern California, Georgios Petrou University of Southern California, Rajeev Alur University of Pennsylvania, Mayur Naik University of Pennsylvania, Mukund Raghothaman University of Southern California DOI | ||
14:18 18mTalk | Data Extraction via Semantic Regular Expression Synthesis OOPSLA Jocelyn (Qiaochu) Chen University of Texas at Austin, Arko Banerjee University of Texas at Austin, Çağatay Demiralp Massachusetts Institute of Technology, Greg Durrett University of Texas at Austin, Işıl Dillig University of Texas at Austin DOI | ||
14:36 18mTalk | Synthesizing Efficient Memoization Algorithms OOPSLA DOI | ||
14:54 18mTalk | Algebro-geometric Algorithms for Template-Based Synthesis of Polynomial Programs OOPSLA Amir Kafshdar Goharshady Hong Kong University of Science and Technology, S. Hitarth Hong Kong University of Science and Technology, Fatemeh Mohammadi KU Leuven, Harshit Jitendra Motwani Ghent University DOI | ||
15:12 18mTalk | Modular Component-Based Quantum Circuit Synthesis OOPSLA DOI |