Work

I'm a senior researcher at Certora

Research

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.

Other than the work in my dissertation, I also got to hack on:

Publications

Practical Verification of Smart Contracts using Memory Splitting - OOPSLA 2024 [pdf]

with Shelly Grossman, John Toman, Sameer Arora, Mooly Sagiv, and Chandrakana Nandi

Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs - POPL 2019 [pdf]

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

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.

I earned my Ph.D. after six years in the Programming Systems group at UCSD.

After earning my Ph.D., I was a senior engineer at Qualcomm, where I worked on maintaining the compiler for the Adreno family of GPUs, supporting the OpenGL and Vulkan front- and middle-ends.