My research interests are in logic and semantics of computation, and in automated tools for program verification and analysis.
With John Reynolds I developed separation logic, which addresses the problem of tractable reasoning about the mutation of data structures in computer memory. With David Pym I developed bunched logic, a general logic of resource, which is a more abstract cousin of and precursor to separation logic. I proposed a concurrent separation logic, which has made inroads on the problem of modular reasoning about shared-memory concurrent programs.
In much of my work I have been interested in the concept of locality, the idea that programmers look at state in little pieces rather than keeping track of the entire global state. I proposed a connection between parametric polymorphism and local state in a JACM'95 paper with Bob Tennent. This spurred some of my later work on separation logic and the frame problem and what I called "local reasoning", that you can reason about a piece of code by talking only about the resources it touches instead of tracking the entire global state of a system.
In recent years I've gotten involved in software tools research, particularly with the SpaceInvader team (Cristiano Calcagno, Dino Distefano, Hongseok Yang and I) when we were all in London and our SLAyer/TERMINATOR colleagues at Microsoft Cambridge (Josh Berdine, Byron Cook). Eventually, the local reasoning idea was ported to program analysis, by using a variation on abductive inference to approximate a program's footprint, and this allowed a certain kind of automatic program analysis to scale to millions lines of code, where previously only hundreds or a few thousands were possible (see new JACM'11 bi-abduction paper).
Of late I've also been paying attention to some of the fascinatingly intricate fine-grained concurrent algorithms, and to abstract models of consurrency. Despite decades of work, there are absolutely basic, unsolved problems in concurrency, and the problems are becoming all the more urgent because of developments in chip design.
Concurrency and automated analysis are both vibrant research areas, with unsolved, basic problems, and this is where my main current interests lie. There is a tremendous amount of work to be done in both of these areas. And when one combines the two, analyzing or verifying concurrent programs, the problems become even harder, which is to say as well more interesting.
See also this research portrait from a chat with Wendy M Grossman.
Separation Logic
Smallfoot
SpaceInvader
Abductor
Attack of the 50 Foot Spatial Dudes
Proof of Cyclic List Reversal