Program synthesis is the problem of automatically discovering programs from specifications of their intended functionality. Such specifications can take various forms, including noisy input-output examples, desired program trajectories, behavioral constraints written in first-order or temporal logic, and visual or textual descriptions of the program’s goals. Program synthesis cuts across most of our lab’s research. In some cases, we are motivated by the potential of program synthesis to make programming more productive. In other cases, our goal is to synthesize programs that model, and help us understand better, the real world.

In either case, one faces two basic issues. First, a program synthesizer needs to search through a space of programs that is combinatorial and quickly explodes. Second, specifications are often ambiguous or incomplete, and this means that not all programs that meet the specification are interesting. Over the years, we have developed many approaches to these challenges. For example, some of our methods prune a search space of programs using automated deduction techniques. Others guide a discrete search over programs using learned statistical models. Yet others relax the space of programs into a continuous space that can be explored with scalable gradient-based optimization.

---

Selected Publications