| My interests lie in the application of
programming languages techniques to improve reliability
of software. More specifically, I am interested in
static program analysis, and its application to
compilers, error detection tools and program
verification systems. Static program analysis is any
method for automatically over-approximating runtime
behavior of a program. Examples of program analysis
methods are type inference, dataflow analysis, model
checking, and theorem proving.
I believe that as more and more aspects of our lives
are controlled by software, correctness will become a
major concern for all producers of software. This is
especially true for providers of platform software.
Correctness is a domain of opportunity for static
analysis; every other method for enforcing correctness
is either incomplete (testing, partial simulation,
runtime error detection) or involves high programmer
overhead (new languages and type systems).
Unfortunately, precise static analysis of large software
has, to this point, proven intractable.
My research is guided by two basic insights: First,
if an analysis problem if broken up into its constituent
components, it is possible to produce a scalable
analysis solution by choosing the right mix of expensive
and cheap analyses targeted at the appropriate
subproblems. Second, practical scalable analysis must
run on real code written by real programmers, not
imaginary code written on whiteboards by researchers. In
other words, the space of programs written in practice
is much smaller than the space of programs. This insight
leads to a simple approach to designing scalable program
analyses: Given a problem, identify a cheap algorithm
that produces inaccurate results, and an expensive
algorithm that produces accurate results. Based on
examination of coding practices, design an algorithm in
between the two extremes that trades a little accuracy
for a lot of scalability, by retaining accuracy on the
common cases found in real code. My previous work on
scalable alias analysis algorithms exemplifies this
approach.
More recently, I have applied the same approach to
the problem of verifying the correctness of software wrt
partial specifications of correct behavior. I lead the ESP
project at MSR. I started this project in May 2001,
on the premise that a mixture of cheap global static
analysis and expensive local state space exploration can
be used to accurately identify errors in large programs. |
am
a Researcher in the 
