With George Necula, Evan Chang, and Robert Schneck, I've worked on improving the efficiency of extensible proof-carrying code systems. Our work centers on replacing the transmission and checking of monolithic proofs of program safety with custom, re-usable program analysis tools that justify the trustworthyness of their decisions in different ways. With the Open Verifier project, we proposed a particular online decomposition of proof obligations traditionally encountered in foundational proof-carrying code, guided by a trusted abstract interpretation engine. In our follow-on work on certified verifiers, we instead proposed proving the soundness of program analysis tools once and for all, using a computer proof assistant like Coq.
In both of these projects, I developed complete soundness proofs in Coq for large fragments of x86 Typed Assembly Language.
Interactive computer theorem proving
Most of the research I do today involves some interactive theorem proving. With George Necula, I've worked on making interactive proving easier by creating an interface to George's Nelson-Oppen-style automated theorem prover Kettle. Our implementation supports a novel cooperation mode where a proving task is bounced back and forth between the automated and human provers, as the automated prover identifies useful case splits, discharges some cases automatically, and leaves the rest for the user to prove recursively.
As a summer intern in the Software Productivity Tools group at Microsoft Research Redmond, I worked with my mentor Manuel Fähndrich on the bytecode verifier for the Singularity research operating system. Singularity is novel for its almost total reliance on .NET managed code, even for "systems" code. Static verification of all installed software is a critical part of the Singularity security model, including checking manual memory management and proper adherence to inter-process message-passing protocols. I developed an extensible .NET bytecode verifier and implemented checking for those properties and more.
Software model checking
I've done some implementation work in the BLAST model checker project with Tom Henzinger, Ranjit Jhala, Rupak Majumdar, and Dirk Beyer. I implemented the BLAST specification language, for instrumenting C programs with monitoring code. I added context-free reachability support. I wrote some of the basic support behind automatic model-checking-guided test case generation and combining relational and reachability queries about programs.
Typed compiler intermediate languages
At CMU, I worked with Bob Harper and Leaf Petersen on the TILT type-preserving Standard ML compiler project. I implemented some improvements to some of the intermediate languages, and we developed strict bidirectional type-checking to make type inference more effective on the flattened ML-like terms found in TILT and similar compilers.