About Me

My Picture

I am a Ph.D student in Computer Science, working at the University of California, San Diego since the fall of 2014.

My research interests cluster around software verification: that is, using mathematical and logical tools to improve the quality of essential software. My interests span both interactive and automated theorem proving: I care about building powerful domains admitting automatic reasoning just as much as I care about helping the people who still need to build proofs manually.

I am driven by a belief that as software becomes a more and more central part of our world, we need to upgrade the tools we use to ensure our software is going to behave correctly. From medical devices to blockchains to smart infrastructure, software has the potential to greatly improve our lives - but only if we can get it right.

Projects

I’m currently working on verification of Hierarchical Artifact Systems, a powerful yet decidable formalism for specifying certain classes of relational, data-oriented systems and rich properties about them.

I’ve contributed to Mirror-Core, a library for reflecive proof automation in Coq.

Previously at UCSD, I was involved in the VeriDrone project, working to use the Coq proof assistant to verify control software for a Pixhawk PX4-based quadrotor.

As an undergraduate at Princeton I worked on improving proof automation in the Verified Software Toolchain. It was there that I got my first taste of the thrill of verification - one I have been chasing ever since.