Het onderzoek van de groep van Krebbers richt zich op het veilig en betrouwbaar maken van software door middel van wiskundige bewijzen. Zijn groep houdt zich bezig met het doorgronden van de semantiek van veelgebruikte programmeertalen zoals Rust, C en OCaml, zonder daarbij de lastige details zoals pointers, excepties en parallellisme uit de weg te gaan. Op basis van deze semantiek ontwerpt zijn groep verificatiemethoden die worden geïmplementeerd als open-source-tools. Een belangrijk doel is om verificatie “modulair” te maken, zodat programma’s stuk voor stuk kunnen worden geverifieerd, wat schaalbaarheid mogelijk maakt. Deze methoden en tools zijn gebaseerd op wiskundige logica en worden zelf geverifieerd met behulp van bewijsassistenten: computerprogramma’s die de juistheid van wiskundige bewijzen controleren.
De groep van Krebbers werkt ook aan de ontwikkeling van de fundamenten voor de volgende generatie programmeertalen en typesystemen. Het doel is om zoveel mogelijk programmeerfouten al tijdens het compileren op te sporen. In zijn ERC Consolidator-project bestudeert zijn groep dit probleem in de context van computerprogramma’s waarin meerdere taken in parallel worden uitgevoerd.
Krebbers is geïnteresseerd in het moderniseren van het programmeeronderwijs binnen het curriculum van de informatica. Samen met zijn collega’s herontwerpt hij de programmeercursus voor eerstejaarsstudenten, waarbij gebruik wordt gemaakt van de nieuwe programmeertaal Rust, die fouten op het gebied van geheugenveiligheid automatisch detecteert.
Over Robbert Krebbers
Prof. dr. Robbert Krebbers (geboren in 1987 in Groesbeek) begon zijn academische loopbaan aan de Radboud Universiteit, waar hij zijn bachelor- en masterdiploma in informatica behaalde. In 2011 startte hij zijn promotietraject, waarin hij zich verdiepte in de wiskundige semantiek en programma-verificatietechnieken voor de veelgebruikte programmeertaal C. In 2015 promoveerde hij cum laude op zijn proefschrift “The C standard formalized in Rocq.”
Na het afronden van zijn promotie werkte Krebbers tot 2016 als postdoctoraal onderzoeker bij de groep logica en semantiek aan de Universiteit van Aarhus in Denemarken. Vervolgens werd hij benoemd tot universitair docent bij de groep programmeertalen aan de TU Delft, waar hij tot 2020 werkzaam was. Daarna werkte hij als universitair docent aan de Radboud Universiteit en werd hij daar in 2021 benoemd tot universitair hoofddocent.
Tijdens zijn postdoc was Krebbers medeoprichter van het Iris-framework voor programma-verificatie, een actief open-sourceproject dat hij tot op de dag van vandaag mede leidt. Samen met zijn Iris-collega’s ontving Krebbers in 2023 de Alonzo Church-prijs voor de meest invloedrijke bijdrage aan logica en computationele wetenschappen in de afgelopen 25 jaar. Ook ontving hij in 2024 een ERC Consolidator Beurs voor het COCONUT-project, dat zich richt op de ontwikkeling van correcte concurrente software met behulp van typen. In 2026 won hij de Nederlandse Prijs voor ICT-Onderzoek voor innovatief onderzoek.