My research interests include the semantics, analysis, and correctness of programs, especially concurrent programs. I've done work in compiler and program verification, programming language semantics for low-level languages, and formalizing memory models (both sequential and concurrent). My main tools are the interactive theorem provers Coq and Isabelle.

I am working on building tools and techniques for proving the correctness of concurrent C programs, using the Verified Software Toolchain and Iris. I aim to prove correctness of realistic concurrent systems code, including web server and database implementations, and to develop simpler approaches to reasoning about fine-grained concurrency. I've written an introduction to verifying concurrent programs in VST.

More generally, I'm interested in bridging the gap between programming and program verification, providing better tools for programmers to understand the effects of code as they write it, and making it easier to verify code as it's written. I'd like to make it possible for every C programmer to write proved-correct code. This means thinking about the user experience of verification, not just writing proofs ourselves. If this sounds interesting to you, let me know!

 

Current Projects: