Project Ideas

Here are some project ideas, roughly in the order of increasing difficulty / scope. For all projects that involve applying synthesis in a new domain, the default is to use an existing synthesis framework such as Sketch, Rosette, or PROSE, but you can also implement a synthesizer from scratch if you feel up to task. You can also take a look at the completed projects and implement an alternative solution for one of them. Please talk to us before deciding on your project topic.

• CEGIS: Re-implement a symbolic program synthesizer based on a CEGIS loop. Your synthesizer must accept input in the Sygus format.
• VSA: Re-implement a basic version of FlashFill based on VSAs. Your synthesizer must be able to solve benchmarks from the PBE-Strings track of the Sygus competition.
• And-Or Euphony: Euphony represents a solution to the synthesis problem as a path in a graph of sentential forms, and uses the A* algorithm to search for the shortest path. An alternative (more compact) representation of a solution is with an And-Or Tree, where and-nodes are sentential forms and or-nodes are non-terminals with context. The goal of this project is to apply the AO* algorithm, an extension of A* to And-Or trees, to this problem and investigate whether it leads to more efficient synthesis.
• Library Learning with Equality Saturation: Equality saturation and e-graphs have been recently used to extract structure from CAD models. On the other hand, there's work on library learning that has a similar problem statement but uses more ad-hoc techniques. The goal of this project is to apply equality saturation to the setting of library learning.
• ARC: Implement a synthesizer that solves (a simple subset of) tasks from the Abstraction and Reasoning Challenge.