Current projects:

Automated programming revisited

Programmers cannot live without syntax checkers, type checkers and editor auto-completion. These are useful tools but they hardly exploit the vast computer power at our disposal. We are developing computer-aided programming that brings the computational power to the process of constructing programs. We pose this problem as synthesis of programs from multi-modal specifications: templates of programs, declarative assertions, executable specifications, examples and demonstrations. We are developing synthesis theories and algorithms, language constructs and tools that embed synthesis into the programming process.

Parallel, low-power web browsers

Web browsers popularized smart phones but—unlike on laptops—failed to gain dominance as the application platform. The reason is that browsers are prohibitively slow on the power-constrained mobile devices. As a workaround, mobile applications are developed in the more efficient frameworks such as Android, iPhone SDK or Silverlight. These frameworks are not only less productive but also give rise to platform balkanization which hampers the application progress compared to we had seen in early Web 2.0, which enjoyed the unified platform of the web browser. This project investigates future browsers from two perspectives: energy-efficient implementation of the browser and programmability of client applications.

Program synthesis for biology

Recently, my group began work on synthesis of concurrent programs that model how stem cells determine their fate. We also started work on synthesis of metabolic pathways.

Hack your language!

Hack Your Language! is a senior course (CS164) on programming languages in which students build their own coroutine interpeter, parser generator, and a web browser. These projects are vehicles for learning modern software design principles; we design new programming abstractions and embody them in small, domain-specific languages (DSLs). Students construct DSLs to help in the construction of their browsers and also extend the browser with small languages for DOM manipulation (a'la jQuery) as well as a reactive language (a'la Rx) . As a final project, students design and implement a DSL of their own choice.

Past projects:

Program analysis and tools enabled by program analysis

My group solved two long-standing problems in program analysis and debugging, both through a new understanding of the structure of computer programs. Our first result is the first fully context-sensitive algorithm for pointer analysis. Our refinement-based algorithm is both 60% more precise (in its false alarms) and more memory efficient (100 to 1000-times) than the state of the art. The precision of pointer analysis, also known as flow analysis, dramatically influences the usefulness of programmer tools. In particular, context-sensitivity, which is necessary for today’s programs built from components, was previously obtainable only partially, and required to be executed overnight. Our second result was a new definition of the program slice. We introduced the thin slice, which factors the classical slice into a programmer-explorable hierarchy. By separating where the value flows from why it flows that way, the thin slice allows the programmer to comprehend the program gradually, refining the thin slice as needed; in the limit, thin slice grows to the classical slice. Thin slices are 3 to 10-times smaller than traditional slices.

BAFL: Bottleneck Analysis of Fine-grain Parallelism

This project developed bottleneck analysis for parallel processors. We developed algorithms and evaluated hardware designs for understanding of the critical path in modern processors. The notion of critical path had been used to informally (and often incorrectly) to evaluate and justify designs; we showed how to model it correctly and compute it efficiently [Fields et al, ISCA’01, ISCA’02].

Dynamic program analysis and debugging

Our project, co-led with Mark Hill, has been credited for starting a line of recent research in the area of hardware-supported deterministic replay. The goal of another effort was to make it possible for programmers to write assertions that test deep properties. These assertions are too expensive to execute traditionally; we have shown how to develop an automatic incrementalizer of data structure consistency checks, such as the test of the Red-Black Tree property. An incrementalized check reuses computations from previous invocations of the check, accelerating checks by orders of magnitude [Shankar, PLDI 2007].

Path-sensitive value-flow analysis and optimizations

This project developed one of the first path-sensitive program analyses, both static and profile-directed.

About

News

Emina Torlak and I have given an invited tutorial at CAV 2012. The tutorial is being expanded this semester into a graduate course, which you can follow as we add lectures and homeworks. CAV tutorial slides: (ppt, pdf, screencast). The graduate course.

Postdoc position position in synthetic biology

8/13/2012

We are looking for postdocs in synthetic biology. We need curious, well-rounded computer scientists with expertise in algorithms, hacking, and with interest in biology.

NSF Expedition in Computing for program synthesis

4/3/2012

The multi-university ExCAPE project aims to change computer programming from the tedious task to one in which a programmer and an "automated program synthesis tool" collaborate to generate software that meets its specifications.

Looking for a postdoc position?