Who am I

• Program Synthesis and Verification
• Languages and tools for parallel programming
• Program analysis

Research Agenda

I want to exploit the growing availability of computing power and the increasing maturity of formal methods to make programming easier.

My current focus is on program synthesis; a technology that promises to automate the mechanics of implementation, freeing programmers to focus on higher-level concerns.

As part of my research I have developed sketching, a new approach to synthesis that promises to bring synthesis within the reach of mainstream programmers.

Sketching: Synthesis from partial programs

Sketching provides a fresh answer to a long-standing concern in user-directed synthesis: how to exploit the programmer's expertise to reduce the burden on the synthesizer.

The novelty of sketching is that the programmer communicates her insight with a partial program rather than with domain axioms. This allows the programmer to control the cost of synthesis in a natural way, without resorting to new formalisms.

• The use of partial programs as an interface for user-directed syntehesis (PLDI 05). 
• The development of a combinatorial synthesis algorithm to synthesize implementations from partial programs (ASPLOS 06).
• The design and implementation of the SKETCH language (ASPLOS 06).
• The use of problem reduction to incorporate domain knowledge into a general combinatorial synthesis procedure (PLDI 07)
• A generalization of sketching to the domain of concurrent datastructures (PLDI 08).