Registered user since Thu 16 Jun 2016
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).
- Author of (PLDI 2021) RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types within the SIGPLAN Track-track
- Author of (PLDI 2021) Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic within the SIGPLAN Track-track
- Author of Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris within the PLDI-track
- Author of Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic within the POPL-track
- Author of VIP: Verifying Real-World C Idioms with Integer-Pointer Casts within the POPL-track
- Author of Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations within the POPL-track
- Author of Knowing When to Ask: Artifact within the OOPSLA Artifacts-track
- Author of Knowing When to Ask: Sound Scheduling of Name Resolution in Type Checkers Derived from Declarative Specifications within the OOPSLA-track
- Author of Knowing When to Ask: Sound Scheduling of Name Resolution in Type Checkers Derived from Declarative Specifications within the Posters-track
- Author of Intrinsically-Typed Definitional Interpreters within the Artifact Evaluation-track
- Author of Iris - A Modular Foundation for Higher-Order Concurrent Separation Logic. within the TutorialFest-track
- Author of Intrinsically-Typed Definitional Interpreters for Imperative Languages within the Research Papers-track
- Author of RustBelt: Securing the Foundations of the Rust Programming Language within the Artifact Evaluation-track
- Author of RustBelt: Securing the Foundations of the Rust Programming Language within the Research Papers-track