I'm interested in tools and techniques for building reliable software. As a graduate student, my work focused on refinement type-based approaches to verifying memory safety and functional correctness which place a low annotation burden on the programmer.
I now work at Google NYC. While at UCSD, my advisor was the incredible Ranjit Jhala.
Dissertation
publications
talk slides
Low-Level Liquid Types
POPL 2010
Type-Based Data Structure Verification
PLDI 2009
Liquid Types
PLDI 2008
projects
CSolve
A verifier for C programs based on Low-Level Liquid Type inference.
DSolve
A verifier for OCaml programs based on Liquid Type inference and type-based data structure verification.