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.
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.
Tools for computational “doing”
Computer-aided programming and data manipulation for scientists and end users.