I am interested in programming language, compiler, and program analysis technology.
Below are some of the projects I've worked on.
For more information about my research, check out my
publications and talks.
Scripting languages include features that frustrate
static reasoning, such as extensible objects, dynamically computed
keys, loosely coupled recursion, reflection, and dynamic code loading.
This project aims to develop type systems to
describe idiomatic programs in scripting languages
[Staged Information Flow]
The prevalence of dynamically loaded code makes program analysis for
We present a staged approach to tracking information flow that splits the
analysis burden between compile-time and run-time.
[Fine, Microsoft Research]
Modern SMT solvers allow refinement type systems to track security
and other complex properties, but they become a large part of the
compiler's trusted computing base (TCB). Fine incorporates a type-preserving
translation to eliminate the solver from the TCB.
Fine is a precursor to MSR's
Defining a dataflow analysis for concurrent programs is complicated
by the subleties of thread interleavings and locking protocols.
Radar automatically converts a sequential dataflow analysis to a
concurrent one by making use of datarace information from the
Relay race detector for C programs.