Error-free computer thanks to math and logic

What if computer programmers had autocorrect at their disposal, a tool that could detect program errors and suggest changes? Jorge Pérez, associate professor in Software Foundations at the University of Groningen, uses mathematics and logic on a quest towards a world free of software errors. A world in which programs no longer crash and critical services such as hospitals and airports never have to face software problems like the one witnessed earlier this year.

 FSE Science Newsroom | René Fransen

‘Software errors can be costly, and in some cases even catastrophic,’ says Pérez. ‘But writing correct programs is difficult, even for experienced programmers.’ For decades, programmers would simply test their software to detect errors. However, this is not sufficient: ‘Testing can only reveal the presence of errors – it cannot guarantee their absence.’ Because software is ubiquitous, defective programs can result in all sorts of unforeseen consequences.

Multi-tasking software, error-free by design

One challenge is that modern software can execute multiple instructions simultaneously—a feature that is called concurrency.  Web shops, for example, use concurrency to accommodate millions of clients who browse products, pay for orders, and write reviews – all at the same time. ‘Concurrency is a great thing: it is what makes our phones and laptops fast. But programs that involve concurrency are hard to get right, as we humans tend to think sequentially, one task after another.’

It is therefore difficult for software developers to program these concurrent tasks correctly and  anticipate how multiple things may run in parallel. Pérez uses mathematics and logic to figure out how well these tasks are performed in complex situations: ‘Using a mathematical approach to correctness, we can accurately express the intention of the instructions in a program. This allows us to check whether these instructions, and ultimately entire programs and systems, work as intended.’ Perez specializes in mathematical models of programs that make use of concurrency. ‘We use these models to determine how realistic it is for programs using concurrency to run without errors.’ 

This approach guides the development of new methods for eliminating subtle program errors. ‘Ideally, we would like to create something similar to the autocorrect feature in Google Docs, which detects errors and suggests changes’, Pérez says. Although computer languages are more limited than natural languages, this is not an easy task. ‘Software systems are complex: they are built by integrating different programs, much like assembling a LEGO set. These programs are large, run on different computers across the world, and use different technologies. We address this complexity by devising rigorous methods that help write programs that are error-free by design. This was precisely the topic of my VIDI project.’

Collaboration and public engagement

Pérez works on these problems together with his students and colleagues in the Fundamental Computing group, as well as within the collaborative network of Dutch theoretical computer scientists, NetTCS. Not only does he collaborate with his peers on these challenges, but he also engages the general public on the importance of properly functioning software. ‘I am especially proud of a teaching package for secondary schools, which I helped develop.’ The package teaches pupils how software works and how it can go wrong (in Dutch). ‘I have also given talks at science festivals like Noorderzon and produced several video animations on the importance of software verification.’ 

His approach can improve the reliability of complex software systems. Could this eventually lead to error-free software? ‘That is my ultimate goal’, he says. ‘Because I think that we computer scientists have a responsibility.’ It may seem daunting, but Pérez is not fazed: ‘The future is exciting. There is more awareness about the importance of reliable software for society, and the industry is increasingly interested in mathematically verified software.’

See also the home page of Jorge Pérez and his full CV.