I am a systems researcher with a focus on correctness, distributed systems, and security.
I believe verification technology is rapidly approaching the point where, for high-value systems, test-driven development can be largely replaced with verification-driven development. Imagine shipping software with zero safety bugs in its implementation. The primary challenge is to reduce the cost of verification, making it practical and accessible to the practicing engineer. The next research step is to gain experience with more complex, realistic scale development efforts that push the boundaries of today's tools and methodologies.
To pursue this goal:
- I build research systems with high performance and maintainable code to exercise the verification tools, identify common causes of tedium, and feed back improvements. We're building a fast, verified storage system (see "Storage Systems" paper under publications). Our efforts have spawned new a verification language Verus, a new concurrency framework, and new features for Dafny.
- I introduce engineers and students to verification tools to understand what makes the learning curve steep, again so we can improve tool and language design. This includes building an introductory curriculum currently offered as a summer school. This school has launched several smaller protocol-level verification efforts at VMware, giving us feedback from working engineer on what is most challenging about today's tools.
- Inside VMware, engineers use these results to verify protocols, producing a "design doc with a regression test", for our Concord BFT protocol, for a cluster database membership management protocol, and for an FPGA task scheduling protocol.
My past work on refactoring legacy applications into minimal isolation containers was honored with a 2022 ASPLOS Influential Paper Award. To dive deeper into this line of work, I recommend fast-forwarding to this NSDI best paper.
I co-chaired NSDI 2017 and OSDI 2020.
I hold a Graduate Faculty appointment at University of Washington. I taught Distributed Systems there in Spring 2019.
I serve on the NSDI and OSDI steering committees.
I have served on PCs for NSDI, OSDI, SOSP, ATC, ICDCS, FAST, and VEE; I am presently serving on ATC22 and NSDI23.
I have served on thesis committees for Ray Cheng, Sangmin Lee, Shih-Wei Li,
and Luke Nelson.