Hi! I’m William Mansky, and I’m interested in expanding the boundaries of provably correct software.
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:
- Iris in VST: integrating features of the Iris separation logic framework into the Verified Software Toolchain for C programs
- Verifying single-node database implementations, with Lennart Beringer‘s team at Princeton
- Connecting verified C programs to verified operating systems, with the DeepSpec team
- Developing specifications for weak-memory libraries, with the extended Iris team
- Proving correctness of concurrent programs with C11 atomic operations