Traditional systems programming languages such as C and C++ are notorious for undefined behavior: if you perform an illegal action such as dereferencing an invalid pointer, the program might do anything (crash, cause data corruption, leak your passwords). This plagues C and C++ programs with subtle bugs and security issues that are hard to detect (the bad). While being a burden for programmers, undefined behavior is important to allow compilers to generate very efficient code (the ugly). Fortunately, modern systems programming languages such as Rust allow for the best of both worlds: their static type system guarantees the absence of undefined behavior, and their efficiency is similar to C or C++ (the good).

In this talk I will explain the good/bad/ugly of undefined behavior, how it can be formalized in a mathematical specification (semantics) of a program language, and how it is used in correctness proofs of compilers and type systems mechanized in proof assistants such as Coq.

I am an associate professor at the department of software science at Radboud University Nijmegen, The Netherlands.

My research is centered around scaling up program verification techniques to challenging programming paradigms like concurrency, higher-order functions and modules, and applying these techniques to programming languages like C, Rust, and Scala. I like to build solid mathematical foundations and usable tools, preferably using the Coq proof assistant.

The main research project I am the co-designer and co-leader of is Iris: a framework for concurrent separation logic in Coq. Iris has been deployed in a wide variety of verification projects, for many different programming languages, at many different institutes world-wide. Check out the Iris website for more information!

I have received my PhD (cum laude) from Radboud University Nijmegen (2011-2015), have been a postdoc in the logic and semantics group at Aarhus University (2015-2016), and an assistant professor in the programming languages group at Delft University of Technology (2016-2020).