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.
• Bottom-up enumeration in egg: Bottom-up enumeration with observation equivalence reduction stores all the programs it has enumerated in program bank. It also discards observationally-equivalent terms, so there is no way to generate more than one program that satisfies all the examples. The idea of this project is to re-implement bottom-up enumeration, but store all enumerated terms in an e-graph, using the efficient egg library. The research question is whether e-graphs provide enough compression to let us store all explored terms, as opposed to only a single representative of every equivalence class.
• Extending SuSLik SuSLik is a synthesizer we developed that generates low-level pointer-manipulating programs from separation logic specifications. There are several exciting directions for extending this work:
  • More expressive specifications: Right now you can only use integers and sets in your specs. For example, I can ask SuSLik to synthesize a procedure for copying a linked list that preserves the set of list elements, but there will be no guarantee that it preserves the order of elements. To address this limitation, in this project, you will extend SuSLik to also support sequences in specifications.
  • Support for loops: SusLik currently only synthesizes recursive programs, and cannot synthesize loops. The goal of this project would be to extend SuSLik to support loops. The easiest way to do this is to modify the rule for generating recursive calls in such a way that it only generates tail calls, and then syntactically transform tail recursion into loops. This is non-trivial, however, because the rule for generating tail calls has to be guided by the postcondition (SuSLik's current call rule is guided by the precondition).
  • Synthesizing efficient programs: SuSLik (see above) synthesizes programs that are provably correct, but might be inefficient: for example, if you ask it to flatten a tree into a doubly-linked list, it synthesizes a quadratic implementation, even though a linear one can also be synthesized (with manual guidance). The goal of this project would be to integrate resource annotations into SuSLik, so that the user can specify constraints on the performance of the target program (e.g. specify that they want it to be linear in the size of the input).
• Synthesis-powered linter Say there's a method private int foo(String msg, Settings settings) in my code, and I need to add some logging inside foo, so I change the signature to private int foo(String msg, Settings settings, Logger logger). But what I didn't realize is that the logger objects could actually be reached from settings, e.g. via settings.global.logger. The goal of this project is to build a linter that, given a change like the one above, tries to synthesize an expression of type Logger from the arguments already at hand (in this case, settings.global.logger is the solution), and if the solution is found, flags the change as potentially superfluous.
• Pragmatic communication: There's recent work on synthesis with pragmatic communication, where informally the main idea is to extract more information from positive examples of program behavior using the observation that the user is likely to provide the "simplest" examples or "corner cases". In the original paper, they consider a simple graphical language. In this project the goal would be to explore applications of this idea to other domain, for example, synthesizing regular expressions from only positive examples.
• ARC: Implement a synthesizer that solves (a simple subset of) tasks from the Abstraction and Reasoning Challenge.