Derek Dreyer

Scalable Foundations for Verified Systems Programming

The past few decades have seen tremendous advances in program verification technology, with landmark projects like CompCert, seL4, and CertiKOS changing popular perceptions about the feasibility of formal verification for realistic software systems.  But we still have a long way to go until verification tools can be placed in the hands of ordinary programmers.

In this talk, I present two projects -- Iris and RustBelt -- which my students and collaborators and I have been pursuing over the past 8 years toward the goal of building more accessible and extensible verification technology for systems programming applications.  Proposed initially in 2015, Iris is a system for developing and deploying higher-order concurrent separation logics; though only 7 years old, it has already been used in over 60 papers published in top venues in programming languages.  One of the most significant applications of Iris is RustBelt, which constitutes the first formal, machine-checked foundation for verifying the safety of the increasingly popular systems programming language Rust.  In the talk, I will briefly summarize these projects and then suggest several promising directions for future work.

back to overview

Watch Recording
 

Biography

Derek Dreyer is a scientific director and professor of computer science at the Max Planck Institute for Software Systems (MPI-SWS) in Saarbruecken, Germany, and recipient of the 2017 ACM SIGPLAN Robin Milner Young Researcher Award. His research explores connections between type systems for high-level languages and separation logics for low-level systems programming. Most recently, he and his collaborators have led the development of RustBelt, the first formal foundation for the Rust programming language, and Iris, a unifying framework for higher-order separation logic implemented in Coq.  He also spends an inappropriate amount of time researching Scotch whisky.
Footer

Imprint / Privacy