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 tool is the Coq interactive theorem prover.

I am working on building tools and techniques for proving the correctness of concurrent C programs, using the Verified Software Toolchain (VST) 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 am the main designer of VST 3.0, which rebuilds VST on top of Iris’s simple and general foundations, so we can apply the cutting-edge verification techniques of Iris to actually-running C code.

I’m also 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: