Operating Systems and Compilers

Our work in this field focuses on the application of formal techniques to modern, widely deployed languages and systems. We work primarily in domains and in communities that have a pre-existing focus on correctness and security. Our favorite operating system to work with is OpenBSD, and our work on compilers focuses on verifying compiler frameworks and proof-carrying code.