October 26, 2023
Component-based syntheses aim to generate loop-free programs from a library of components like functions or methods provided by an API. This requires an efficient enumeration in the hypothesis search space to synthesize correct programs against the given specification(s). Even for problems with realistic, mid-sized libraries, the search space is gigantic, and often, type specifications over libraries are weak to guide the search in a naíve fashion. One widely accepted solution is to model the problem in the Petri-net domain over the libraries’ types and use the known Petri-net reachability algorithms to find a solution efficiently. Unfortunately, these approaches become less useful as the solution space becomes sparse, i.e., a few valid paths in the Petri-net lead to a solution. A typical scenario when this happens is when the libraries are large, and the user provides further refinement to the queries, e.g., using i/o example or specifications, or when the solutions are large. This makes most paths in the Petri-net unviable/incorrect, thus causing the synthesizer to struggle in such cases. In this work, we address these challenges and limitations, presenting Hegel, which allows efficient component-based synthesis in a large and sparse search space. At the heart of our approach is a new data structure called Qualified Tree Automata (QTA). We use Qualified Tree Automata to compactly keep track of information about all enumerated terms (failed and non-failed terms) along with similarities between these terms using subtyping, and utilize this information to reduce the search space optimally. We also introduce a new notion of completeness-modulo-similarity, allowing optimal enumeration while guaranteeing completeness. We implement these ideas in a tool called Hegel and compare the approach with the state-of-the-art synthesizers.
About Ashish Mishra
Ashish Mishra is a Postdoctoral Researcher at Purdue University, where he works with Professor Suresh Jagannathan in the areas of Programming Languages, Program Verification, and Program Synthesis.