Rastislav Bodik

Paul G. Allen School of Computer Science & Engineering
University of Washington
Seattle, WA

My research group works on making it easier to write computer programs, mostly using program synthesis, a technique for computer-aided construction of software. Our research agenda is to develop programming languages and tools in which the human is allowed to give incomplete instructions; from these, a complete program is obtained in a dialogue with a “programmer assistant.”

Foundations of program synthesis

With collaborators, my group developed the ideas of algorithmic synthesis using sketches (partial programs) and constraint solving. We have later generalized the ideas to so-called solver-aided languages, which simplify programming by delegating coding tasks to a constraint solver. We also work on mining specifications and synthesis-aided programmer tools.

Rosette and solver-aided domain-specific languages. Our work on algorithmic synthesis (sketching, angelic programming) has evolved into extending small languages with constructs that delegate programmer work to a constraint solver. Rosetter is a host language for SDSL construction, developed by Emina Torlak.

Mining specifications and synthesis of API-level code. Prospector and CodeHint are two synthesizers for construction of code that composes library and framework code.

Large-scale synthesis and rethinking compilers

To scale synthesis to system software, we are developing abstract and modular synthesis algorithms. To facilitate rapid development of advanced compilers, we are exploring the idea of a synthesis-aided compiler.

Synthesis for layout engines. We used abstract synthesis to generate a parallel layout engine for the web browser and data visualization. Currently, we are working on synthesis of an efficient incremental layout algorithm that is also statically parallelizable. A collaboration with Mozilla.
Chlorophyll: a synthesis-aided compiler for spatial architectures. Chlorophyll is a synthesis-aided compiler for spatial architectures. It is testbed for exploring how synthesis can simplify compiler construction. Currently, Chlorophyll synthesizes code for the GreenArrays GA144 processor.
Probabilistic programming languages. Recently, we began work on synthesis-aided compilation of probabilistic programs. A collaboration with CRA and NIMBLE.

Tools for computational “doing”

Computer-aided programming and data manipulation for scientists and end users.

Program synthesis for executable biology. Because many mechanistic models of biological cells can be written as executable programs, synthesis can be used to infer biological models from experimental data.
Web scripting by demonstration. We are designing the stack of components for PBD applications that access and manipulate web data: a deterministic replayer, data scraper, and a synthesizer of relational queries.
Authoring data visualizations. Programming By Manipulation (PBM) seeks to simplify layout programming by guiding the user during the exploration of candidate layouts.