Research

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.

In the past, I have worked on CSolve, which is a verifier for C programs based on Low-Level Liquid Types.

Teaching

Materials for the classes that I have TA'd at UCSD live on github.

Publications

Verification of Distributed Programs via Canonical Sequentialization - OOPSLA 2017 [pdf]

with Klaus v. Gleissenthall, Rami Gökhan Kıcı, and Ranjit Jhala

Predicate Abstraction for Linked Data Structures - VMCAI 2016 [arXiv]

with Ranjit Jhala

Bounded Refinement Types - ICFP 2015 [pdf]

with Niki Vazou and Ranjit Jhala

CSolve: Verifying C with Liquid Types - CAV 2012 (tool description) [pdf]

with Patrick M. Rondon, Ming Kawaguchi, and Ranjit Jhala

Deterministic Parallelism with Liquid Effects - PLDI 2012 [pdf]

with Ming Kawaguchi, Patrick M. Rondon, and Ranjit Jhala

Background

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.