SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Wed 25 Oct 2023 14:36 - 14:54 at Room II - program synthesis 2 Chair(s): Chandrakana Nandi

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 Oct

Displayed time zone: Lisbon change

14:00 - 15:30
program synthesis 2OOPSLA at Room II
Chair(s): Chandrakana Nandi Certora
14:00
18m
Talk
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
18m
Talk
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
18m
Talk
Synthesizing Efficient Memoization Algorithms
OOPSLA
Yican Sun Peking University, Xuanyu Peng Peking University, Yingfei Xiong Peking University
DOI
14:54
18m
Talk
Algebro-geometric Algorithms for Template-Based Synthesis of Polynomial ProgramsDistinguished Paper
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
18m
Talk
Modular Component-Based Quantum Circuit Synthesis
OOPSLA
Chan Gu Kang Korea University, Hakjoo Oh Korea University
DOI