The Group

We are developing formal foundations and tools that establish machine-checked guarantees for real-world software systems. To achieve this, our work spans all the way from foundational and deeply theoretical to applied, from proving theorems to developing tools.

Right now, one of our main goals is to develop the formal foundations for the external pageRustcall_made programming language.  Rust is a promising young systems programming language that is increasingly used to write critical infrastructure (such as operating system componentss, web browsers, or cloud storage backends). Rust provides strong safety guarantees (covering both memory safety and thread safety), but also lets programmers write "unsafe" code to circumvent the limits of what the compiler is able to check. Such unsafe code can interact directly with low-level machine details; the responsibility of upholding safety is now on the programmer. This implies a strong need for a complete, unambiguous, authoritative specification of all of Rust, as well as the ability to verify programs against that specification. In the pursuit of that goal, we work with the Rust project to ensure that our specification reflects the constraint of real-world usage, while also developing the techniques required to even carry out machine-checked specification and verification at the scale of a langugage like Rust.

Learn more about who we are, our research, what we teach, and student projects with our group.