About

I am an assistant professor in the programming languages group at the department of software technology at Delft University of Technology. My research interests span many aspects of program verification, for example:

• Semantics of real programming languages: In my PhD thesis, I have developed a semantics and separation logic for a large fragment of the C programming language. More recently, I have contributed to Rustbelt: the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust.
• Multilingual software: I have recently been awarded a prestigious Dutch NWO Veni grant (250.000 EUR) to work on the semantics and reasoning principles for interaction between different programming languages via shared-memory and asynchronous message passing.
• Concurrent separation logic: I am one of the main developers of the Iris framework for concurrent separation logic in Coq, which has been deployed very effectively in a wide variety of verification projects. These projects include but are not limited to: verification of fine-grained concurrent data structures, logical-relations for relational reasoning, program logics for relaxed memory models, program logics for object capabilities, and a safety proof for a realistic subset of the Rust programming language. Take a look at the Iris website for the many exciting applications of Iris.
• Proof assistants: I am an active user of the Coq proof assistant; nearly all of my research has a corresponding mechanization in Coq. Moreover, I am the main developer of coq-std++: an extended standard library for Coq.
• Tactic languages: In order to carry out proofs at the right level of abstraction, I have worked on the development of various tactics languages for the Coq proof assistant. Notably, I am the designer of the MoSeL (formerly Iris Proof Mode) tactic language for separation logic proofs in Coq, and have contributed to Mtac2, a next-generation tactic language with support for strongly typed tactic programming.

Before becoming an assistant professor at TUDelft, I have received my PhD (cum laude) from Radboud University Nijmegen under the supervision of Freek Wiedijk and Herman Geuvers, and have been a postdoc in Lars Birkedal's group at Aarhus University.

News

• 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.
• I will be on the program committee of ICFP'20.
• Jules Jacobs has joining my team as a PhD student (1 September 2019).
• I am (co-)organizing CoqPL'20 and PLMW'20 (both collocated with POPL'20 in New Orleans).
• I have organized the workshop Effective Verification: Static Analysis Meets Program Logics at the Lorentz Center.
• Paolo Giarrusso has joining my team as a post-doc (1 April 2019).
• Our paper on semi-automated reasoning about non-determinism in C expressions has been accepted at ESOP'19. You can read the paper here.
• I am (co-)organizing CoqPL'19 (collocated with POPL'19 in Lisbon). Please attend!
• Our paper on the Iron separation logic has been accepted at POPL'19. You can read the paper here.
• I have been awarded a prestigious Dutch NWO Veni grant (250.000 EUR).

Research group

PhD students:

• Arjen Rouvoet (co-promotor, promotor: Eelco Visser)
• Dan Frumin (external co-promotor, co-promotor: Freek Wiedijk, promotor: Herman Geuvers)
• Jules Jacobs (co-promotor, promotor: Eelco Visser)

Post-docs:

• Paolo Giarrusso

Alumni:

• Guillaume Ambal (intern from ENS-Lyon)

Contact

Email: (λ x y . mail @ x y . nl) robbert krebbers

Office: room E04.400, Building 28, Van Mourik Broekmanweg 6, Delft

Send mail/packages to:

Dr. Robbert Krebbers
EEMCS, Software Technology
P.O. Box 5031, 2600 GA Delft
The Netherlands