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:
- CSolve, which is a verifier for C programs based on Low-Level Liquid Types, a refinement type system with decidable inference.
- Liquid Haskell, a refinement type system for Haskell programs.
Publications
Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs - POPL 2019 [pdf]
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]
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.