Past Research Projects
One way that current languages help programmers build robust
software systems is by
supporting the creation of reusable
software components.
Mainstream object-oriented (OO)
languages provide such components in
the form of classes.
However, there are several common forms of reuse that classes do not
easily provide.
This project addresses some longstanding extensibility limitations of
classes while maintaining the ability to
modularly typecheck and compile those classes.
Software
MultiJava: Open classes and
multimethod dispatch for Java.
Publications
MultiJava: Design Rationale, Compiler
Implementation, and Applications (TOPLAS 2006)
Curtis Clifton, Todd Millstein, Gary T. Leavens, and Craig Chambers
Reconciling Software Extensibility with
Modular Program Reasoning (Ph.D. dissertation, 2003)
Todd Millstein
Relaxed MultiJava: Balancing Extensibility and Modular
Typechecking (OOPSLA 2003)
Todd Millstein, Mark Reay, and
Craig Chambers
Modular
Typechecking for Hierarchically Extensible Datatypes and
Functions (TOPLAS 2004, ICFP 2002)
Todd Millstein, Colin
Bleckner, and
Craig Chambers
MultiJava: Modular Open Classes and Symmetric Multiple
Dispatch for Java (OOPSLA 2000)
Curtis Clifton, Gary
T. Leavens, Craig Chambers, and Todd Millstein
Modular
Statically Typed Multimethods (I&C 2002, ECOOP '99)
Todd Millstein and Craig
Chambers
Multiple
Dispatch as Dispatch on Tuples (OOPSLA '98)
Gary T. Leavens and Todd
D. Millstein
Compilers are an integral part of the infrastructure relied upon by
programmers, and hence their correctness is critical. Compiler
optimizations are particularly intricate and error-prone, but they are
necessary for achieving good performance of the generated code,
especially for higher-level languages. To increase confidence in
compilers, we have
developed the domain-specific language Cobalt and its successor Rhodium
for writing compiler optimizations. Rhodium
can declaratively express a variety of standard
optimizations, and the language's restricted domain allows us to
automatically prove that these optimizations are correct.
Automated Soundness Proofs for Dataflow Analyses and
Transformations via Local Rules (POPL 2005)
Sorin Lerner,
Todd Millstein, Erika Rice,
and Craig Chambers
Cobalt: A Language for Writing Provably-Sound Compiler
Optimizations (ENTCS 2005)
Sorin Lerner,
Todd Millstein,
and Craig Chambers
Automatically Proving the
Correctness of Compiler Optimizations (PLDI 2003)
Sorin Lerner,
Todd Millstein,
and Craig Chambers
Best Paper Award
This work was performed as part of the SLAM project at
Microsoft Research.
The project aims to automatically validate safety properties
(e.g. that a particular locking protocol is respected) of C code and
is being used to find bugs (and prove the absence of certain kinds of
bugs) in Windows device drivers.
The SLAM process involves the iterative use of three tools.
The papers below describe one of these tools, which
abstracts a set of C procedures to a finite-state model that retains
precise information about a set of predicates of interest. The
finite-state model can then be model checked to determine if the
desired safety properties hold.
Polymorphic
Predicate Abstraction (TOPLAS 2005)
Thomas Ball,
Todd Millstein, and Sriram K. Rajamani
Automatic
Predicate Abstraction of C Programs (PLDI 2001)
Thomas Ball, Rupak
Majumdar, Todd Millstein, and Sriram K. Rajamani
A data integration system is an automated method for querying across
multiple heterogeneous databases in a uniform way. A
mediated schema is created to represent a particular application
domain, and data sources are mapped as views over the mediated schema.
The user asks a query over the mediated schema and the data
integration system reformulates this into a query over the data
sources and executes it. The papers below address some foundational
issues: the first studies the problem of determining
when one query subsumes another
in the data integration setting, and the second describes an
expressive but tractable
language for modeling data sources and mapping them to the
mediated schema.
Query
Containment
for Data Integration Systems (JCSS 2003, PODS 2000)
Todd Millstein, Alon Halevy,
and Marc Friedman
Navigational
Plans for Data Integration (AAAI '99)
Marc Friedman, Alon Levy,
and Todd Millstein
I was a 1999 summer intern of Rustan Leino, working on the
Extended
Static Checking (ESC) project at (the former)
Compaq SRC. The project uses
a lightweight form of program verification technology to statically
detect common programming errors like null dereferences and
out-of-bound array accesses in Java programs.
To perform these checks, ESC asks an
automatic theorem prover to show that a procedure meets its
specification. Rustan, Jim Saxe, and I developed techniques for
translating counterexamples from the theorem prover into meaningful
source-level messages for users. We finally wrote something up
about part of this work several years later.
Generating error traces from verification-condition counterexamples (SCP 2005)
K. Rustan M. Leino,
Todd Millstein, and James B. Saxe
This project involves the solution of classical AI planning problems by
reduction to propositional satisfiability (SAT) problems. The advantage of
this approach is that it can make use of
recent (and continuing) progress in stochastic methods for solving
SAT, thereby potentially enabling faster solutions than
might be otherwise possible in traditional planners. This paper
describes the first automatic planner that employs the SAT approach
(although the idea for the approach pre-dates our work, and is due to
Kautz and Selman)
and evaluates
a space of possible encodings of planning problems into SAT.
Automatic
SAT-Compilation of Planning Problems (IJCAI '97)
Michael D. Ernst,
Todd D.
Millstein, and
Daniel S. Weld
The Medic planner is available
here.