I received my Ph.D. after six years in the Programming Systems group at UCSD.
For my Ph.D. I worked on building tools that automatically prove properties of paramaterized concurrent message-passing programs. The approach works by automatically computing a sequentialized variant of the program that is easier to verify than the naive product construction. The sequential program serves as a proof of shallow properties such as deadlock freedom and local assertion safety. We are currently working on extending our approach to verify deeper functional correctness properties of interesting programs, such as consensus protocols.
Materials for the classes that I have TA'd at UCSD live on github.
Verification of Distributed Programs via Canonical Sequentialization - OOPSLA 2017 [pdf]
Predicate Abstraction for Linked Data Structures - VMCAI 2016 [arXiv]
Bounded Refinement Types - ICFP 2015 [pdf]
CSolve: Verifying C with Liquid Types - CAV 2012 (tool description) [pdf]
Deterministic Parallelism with Liquid Effects - PLDI 2012 [pdf]
I graduated from MIT in 2008 with an S.B. in Computer Science, and again in 2009 with an M.Eng (thesis). After graduation, I worked at Oracle with a fantastic group of people developing a cluster filesystem for Windows, Linux, AIX, and Solaris. It was at this time that I became interested in programming languages and program analysis, especially with respect to analyzing systems software.