Krebbers receives the award together with colleagues from the Max Planck Institute for Software Systems in Germany, Aarhus University in Denmark, ETH Zurich in Switzerland, CNRS Paris in France, and the University of Wrocław in Poland. The researchers received the prize for four publications on the development of the Iris logic, for determining the correctness of computer programs.
Separation logic
A critical challenge faced by computer science researchers is to build computer programs that never crash, never make mistakes, and are secure. In reality, however, this is difficult to achieve because current computer programs are complex and often run several tasks at the same time (in parallel).
Robbert Krebbers' research focuses on the use of mathematical methods to prove that a computer program works correctly. The challenge is to develop mathematical concepts that can handle the complexity of contemporary computer programs and programming languages like Rust, C and Go, such as running parallel tasks. To make this possible, Krebbers and colleagues break up the mathematical proof into separate parts that precisely match up with the parts of the computer program. They use the mathematical concept of separation logic, which is the basis of the Iris logic for which the researchers received the Alonzo Church Award.
Robbert Krebbers: “We can make an analogy between programming a computer program and building a Lego structure. Imagine working with several people on a Lego construction. In that case, it is important that you agree together on how to approach this, so that you do not work against each other. We make a plan with rules for each Lego brick and builder: who is responsible for laying which bricks? This plan prevents mistakes.
With our tool Iris we can make such a plan for the different parts of a computer program: we use mathematical precision to write the logical rules that are necessary to ensure that the computer program works without errors. The use of separation logic allows us to write down the logical rules for each part of the program, rather than the entire computer program. You can then use Iris to check whether each program component complies with the logical rules, and Iris ensures that the entire computer program works without errors.”
Recognition
Iris is now widely used in research. It is also being taken up within the industry: researchers at Meta (from Facebook), JetBrains and BedRock Systems have used Iris to determine the correctness of some of their parallel algorithms. Together with the developers of Iris, and researchers in Cambridge, among others, Krebbers uses Iris to determine the correctness of security-critical parts of Google's Android.
Robbert Krebbers: “Iris started as purely theoretical research, but I am very proud of the practical applications it now has. I think that's why we’ll receive the Alonzo Church Award. A nice recognition for our work!”
The Alonzo Church Award will be presented on 12 July at ICALP 2023 in Paderborn, Germany.