Krebbers ontvangt de prijs samen met collega's van het Max Planck Institute for Software Systems in Duitsland, Aarhus University in Denemarken, ETH Zurich in Zwitserland, CNRS Parijs in Frankrijk, en Universiteit van Wrocław in Polen. De onderzoekers ontvangen de prijs voor vier publicaties over de ontwikkeling van de Iris logica voor het vaststellen van de correctheid van computerprogramma's.
Separation logic
Een belangrijke uitdaging van onderzoekers in de informatica is om computerprogramma's te bouwen die nooit vastlopen, nooit fouten maken én veilig zijn. In de realiteit is dat echter lastig voor elkaar te krijgen omdat huidige computerprogramma's complex zijn en vaak meerdere taken tegelijkertijd (in parallel) uitvoeren.
Het onderzoek van Robbert Krebbers richt zich op het gebruik van wiskundige methoden om te bewijzen dat een computerprogramma goed werkt. De uitdaging hierin is het ontwikkelen van wiskundige concepten die om kunnen gaan met de moeilijkheden van hedendaagse computerprogramma's en programmeertalen als Rust, C en Go, zoals het uitvoeren van taken in parallel. Om dit behapbaar te maken, delen Krebbers en collega’s het wiskundig bewijs op in losse onderdelen die precies overeenkomen met de onderdelen van het computerprogramma. Hiervoor maken ze gebruik van het wiskundige concept van scheidingslogica (separation logic), wat de basis is van de Iris logica waarvoor de onderzoekers de Alonzo Church Award hebben ontvangen.
Robbert Krebbers: “We kunnen een analogie maken tussen het programmeren van een computerprogramma en het bouwen van een Lego-bouwwerk. Stel je voor dat je met meerdere mensen werkt aan een Lego-bouwwerk. Het is dan belangrijk dat je samen goed afspreekt hoe je dat aanpakt, zodat je elkaar niet tegenwerkt. We maken een plan met regels voor elk legosteentje en bouwer: wie is verantwoordelijk voor het leggen van welke steentjes? Door dit plan voorkom je fouten.
Met onze tool Iris kunnen we zo’n plan maken voor de verschillende onderdelen van een computerprogramma: we schrijven met wiskundige precisie de logische regels die nodig zijn om te zorgen dat het computerprogramma foutloos werkt. Het gebruik van scheidingslogica (separation logic) zorgt ervoor dat we de logische regels voor elk programmaonderdeel op kunnen schrijven, in plaats van het hele computerprogramma als geheel. Vervolgens kun je met Iris controleren dat de elk programmaonderdeel aan de logische regels voldoet, en zorgt Iris ervoor dat het computerprogramma in zijn geheel foutloos werkt.”
Erkenning
Inmiddels wordt Iris veel in de logica en programmeertalenwetenschap gebruikt. Ook binnen de industrie wordt het opgepakt: onderzoekers bij Meta (van Facebook), JetBrains en BedRock Systems hebben Iris gebruikt om de correctheid van enkele van hun parallelle algoritmes vast te stellen. Samen met de ontwikkelaars van Iris, en wetenschappers in o.a. Cambridge, gebruikt Krebbers Iris voor het vaststellen van de correctheid van veiligheid-kritieke onderdelen van Google's Android.
Robbert Krebbers: “Iris begon als puur theoretisch onderzoek, maar ik ben erg trots op de praktische toepassingen die het nu heeft. Dat is, denk ik, waarom we de Alonzo Church Award hebben gekregen. Een mooie erkenning voor ons werk!”
De Alonzo Church Award wordt op 12 juli uitgereikt tijdens ICALP 2023 in Paderborn, Duitsland.