Research

My publications contain more technical descriptions of my research.

My research aims to develop tools and techniques to help developers produce more reliable software systems. In particular, I am developing (1) lightweight specification languages, which enable developers to state key properties of their software, and (2) static analysis techniques, which enable compilers to verify that these properties actually hold.

Technology. Static analysis determines properties of a program without actually executing the program; contrast this to dynamic analysis, which collects program properties by observing program executions. Optimizing compilers have used static analysis to eliminate unnecessary computations and thereby speed up program executions. In the software engineering domain, static analysis has been used, for instance, to find potential null pointer bugs and to verify that device drivers always respect API usage requirements.

As a first step towards verifying useful properties on real software, we surveyed a corpus of freely-available Java programs to determine what types of static analysis would help most. Our results allow us to conclude that understanding uses of Java Collections is key to understanding programs; on the other hand, analyzing linked list implementations is less likely to be useful in practice.

Applications. I am particularly interested in using static analysis technology to verify domain-specific properties of software. The key idea is to let the developer state particularly important program properties and then to use static analysis techniques to verify that these properties hold. I believe that the developer has a better chance of understanding the program than anyone else (for example, a static analysis); but that, once the developer states what is important, the computer can proceed to mechanically verify the stated properties. Furthermore, static analysis still works much later in the development lifecycle, long after the original developer has moved on to different projects.

Here are some of my ongoing and past projects:

• DSFinder: applying straightforward static analysis techniques to see how many data structures Java programs implement in practice. (i.e. How much shape analysis do you need to do if you want to understand Java programs?)
• Views: with Brian Demsky, a novel language extension which enables developers to declaratively specify fine-grained (sub-object-level) locking policies.
• Static analysis of tracematches: verifying that specified sequences of program events never occur in any execution.
• Hob: verifying that all executions preserve certain set-based specifications.
• Tokens: embedding design information into Java source code.