Fundamental Computing Group University of Groningen

The power of logic in computation

The Fundamental Computing Group at the University of Groningen uses logic to develop foundations of reliable computing and to prove that software always behaves as intended.

A few years ago, Jorge Pérez, associate professor in software foundations at the University of Groningen, tried to get a digital boarding pass for a flight. The software showed him an error, and he couldn’t get his boarding pass. ‘This most likely happened because something failed in the communication between the various processes involved in producing my boarding pass,’’, explains Pérez. ‘I use a screenshot of the error to explain to my students how software errors still occur, and appear in systems we usually take for granted.’

Pérez specialises in rigorous formalisms for so-called communicating programs, programs that coordinate by sending messages to each other. Communicating programs are embedded in many widely used services, like Amazon or Bol. ‘We users see only a single interface,’, says Pérez, ‘but under the hood, there are many different layers of communicating programs. If I buy something via Bol, my request goes to Bol, Bol communicates with the actual vendor, and the payment proceeds via communication with my bank.’

Pérez is leader of the Fundamental Computing Group, which uses logic to provide foundations for computing in general, and for proving that software is correct. Pérez: ‘We all rely on software being correct and always doing what it is supposed to do. We are frustrated when it does not work correctly. But it goes beyond frustration: incorrect software can have wide-ranging catastrophic consequences for society.’

Both the Fundamental Computing Group and the research in logic have a long and rich history in Groningen. After the recent retirement of a few members, the group entered into a transition phase in which new members had to redefine the group’s research. ‘I see it as an opportunity for us to strengthen our national visibility,’, says Pérez, who himself started eight years ago in Groningen. ‘The new members are full of energy, bring their own networks, and are eager to develop new research directions.’

Pérez finds it important to reach beyond the scientific community. He is a member of the Young Academy Groningen and in cooperation with the Scholierenacademie he developed a teaching package. In addition, the group produced a short animation on software correctness, which was aimed at the general public. Pérez: ‘The teaching package explains to high school students how communicating programs work, how they sometimes do not work and what the consequences may be. Unfortunately, Because because of the pandemic, unfortunately we couldn’t go to schools and discuss the subject with students and their teachers, but we hope this will be possible soon.’

Mathematical toolkit

One of the new group members is Helle Hvid Hansen, who joined in June 2020 as associate professor in logic and semantics of computing. Hansen: ‘I am fascinated by the fundamental relationships between logic and the structure and behaviour of computer programs. My research targets foundational questions that are, central to the rigorous analysis of software, such as: How can we represent and reason about program behaviour? For example, when do two apparently different programs have the same behaviour? Which logics can express relevant properties of programs?’

Hansen specialises in an area called coalgebra. ‘This is a relatively recent discipline that allows different types of program behaviours, for example, nondeterministic, probabilistic, and infinitely-running programs, to be treated in a unified setting. You can think of coalgebra as a rich mathematical toolkit, applicable in multiple situations; you don’t need to rework the theory for each specific class of programs.’

Hansen was attracted to the group, and the University of Groningen more generally, because her research would be well-embedded. ‘My research is connected, but at the same time complementary, to other research expertise in Groningen in formal methods, multi-agent systems and formal philosophy,’, she says. ‘I also like the idea of joining a growing group and being part of setting new directions. I am excited to start working with the new PhDs and postdocs that are joining us in the coming months.’

Sharing memory

Dan Frumin is a postdoc in the Fundamental Computing Group, where he started in October 2020. While he was doing his PhD in Nijmegen, he met Jorge Pérez at a conference. ‘Later, I heard that he was looking for a postdoc for one of his projects,’ says Frumin tells. ‘It was an interesting opportunity for me to join a dynamic, growing group.’

Frumin specialises in logic and verification of concurrent programs that share memory. Frumin: ‘Computers usually run different processes simultaneously that share the same memory. You don’t want to store information that is immediately going to be carelessly overwritten by another process. You need protocols to ensure that the memory will be shared correctly. I work on the verification of such protocols.’

As Frumin, Hansen and other recent hires started their positions in the middle of the pandemic, it was hard to bind the group together in the usual way with in-person activities. ‘We have used Discord, a kind of chat room, for informal interactions and sharing interesting links and content. This has worked quite nicely. But what binds us together the most as a group, is that we all share a common passion for mathematical beauty in applying logic to computation, from different but related perspectives.’

Group passport

Research field
  • Foundations of computing, formal software analysis
Institution
  • The Fundamental Computing Group is part of the Bernoulli Institute for Mathematics, Computer Science and Artificial Intelligence at the University of Groningen (RUG)
Employees as of March 2022
  • 2 associate professors, 1 assistant professor, 2 lecturers, 2 postdocs, 2 emeritus professors, 4 PhD students (plus 3 external PhD students).
More information

Published in I/O Magazine #1 2022
Text Bennie Mols
Images Ivar Pel

March 28, 2022