About
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 currently involved in (and I am leading together with Ralf Jung) 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).
Bachelor and master projects
I am always looking for motivated bachelor and master students. If you are interested in a thesis project related to program languages (in particular, in the field of concurrency, language semantics, separation logic, and Coq), do not hesitate to contact me.
News
- The second edition of the Iris workshop will take place on 2 May–6 May 2022 in Nijmegen.
- My PhD student Arjen Rouvoet defended his thesis Correct By Construction Language Implementations with cum laude distinction (October 2021).
- My PhD student Jonas Kastberg Hinrichsen defended his thesis Sessions and Separation (June 2021).
- Our paper RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types (with Michael Sammler, Rodolphe Lepigre, Kayvan Memarian, Derek Dreyer, and Deepak Garg) received the PLDI'21 Distinguished Paper Award and the PLDI'21 Distinguished Artifact Award (May 2021).
- I have been promoted to associate professor (April 2021).
- My PhD student Dan Frumin defended his thesis Concurrent Separation Logics for Safety, Refinement, and Security (March 2021).
- Our paper Machine-Checked Semantic Session Typing (with Jonas Kastberg Hinrichsen, Daniël Louwrink, and Jesper Bengtson) received the CPP'21 Distinguished Paper Award (December 2020).
- I will move from TUDelft to Radboud University Nijmegen (September 2020).
- Ike Mulder has joined my team as a PhD student (May 2020).
- I have been invited to give a keynote at ADSL'20 (collocated with POPL'20 in New Orleans).
- Together with Lars Birkedal, I am organizing the first edition of the Iris workshop 28 Oct-1 Nov in Aarhus.
- Jules Jacobs has joined my team as a PhD student (September 2019).
- I have organized the workshop Static Analysis Meets Program Logics at the Lorentz Center.
- Paolo Giarrusso has joined my team as a post-doc (April 2019).
- I have been awarded a prestigious Dutch NWO Veni grant (250.000 EUR).
Professional service
PLDI'23 (PC), POPL'23 (PC), ESOP'23 (PC), CPP'23 (senior conference co-chair), PLMW'23 (senior co-chair), Iris'22 (lead organizer), ASL'22 (organizing committee) OOPSLA'22 (PC), CPP'22 (junior conference co-chair), PLMW'22 (senior co-chair), ESOP'21 (PC), FSCD'21 (PC), ICFP'20 (PC), PLMW'20 (junior co-chair), CoqPL'20 (co-chair), PLNL'19 (PC), Iris'19 (co-organizer), Lorentz workshop "Static Analysis Meets Program Logics" (co-organizer), CoqPL'19 (co-chair), POPL'19 (PC), PLNL'18 (co-chair), HOPE'17 (PC), POPL'17 (ERC + AEC), CPP'17 (PC), Coq Workshop'16 (PC).
PhD students and postdocs
Current PhD students:
- Jules Jacobs: daily advisor/co-promotor (promotor: Herman Geuvers)
- Ike Mulder: daily advisor/co-promotor (promotor: Herman Geuvers)
Former PhD students:
- Arjen Rouvoet: daily advisor/co-promotor (promotor: Eelco Visser, 2017-2021, defense October 2021, now postdoc at Delft University of Technology)
PhD thesis: Correct By Construction Language Implementations - Jonas Kastberg Hinrichsen: external advisor (daily advisor at ITU: Jesper Bengtson, 2018-2021, defended June 2021, now postdoc at Aarhus University)
PhD thesis: Sessions and Separation - Dan Frumin: daily advisor/first co-promotor (second co-promotor: Freek Wiedijk, promotor: Herman Geuvers, 2016-2020, defended March 2021, now postdoc at Groningen University)
PhD thesis: Concurrent Separation Logics for Safety, Refinement, and Security
Former postdocs:
- Paolo Giarrusso (2019-2020, now formal methods engineer at BedRock systems)
Contact
Email: (λ x y . mail @ x y . nl) robbert krebbers
Office: Mercator 1, Office 1.17, Toernooiveld 214, Nijmegen
Send snail mail/packages to:
Dr. Robbert Krebbers
Department of Software Science
Institute for Computing and Information Sciences
Faculty of Science
Mailbox 47
PO Box 9010
6500 GL Nijmegen
The Netherlands