My primary interests are theorem proving and formal verification, especially their application to systems software. I am particularly interested in interactive theorem proving for reasoning about concurrency, ownership, and low-level interfaces.

My previous work uses automated program analysis to find resource-management bugs in Linux kernel drivers. More broadly, I am interested in proof assistants, program logics, operating systems, programming languages, and making machine-checked verification useful for code that runs in the real world.