New research project aims to prevent flaws in critical software

Hospitals, banks, and airports—today, software is at the heart of many of society’s critical functions. A new research project, led by Associate Professor at the IT University, Marco Carbone, aims to develop mathematical models to prevent flaws in critical software. The project has recently been awarded 2.8 million kroner from Independent Research Fund Denmark.

Marco Carbone Computer Science Department Research grants innovation programming languages software

Written 17 May, 2021 09:05 by Theis Duelund Jensen

Society depends on critical software, so it is important to develop better ways to ensure that software runs correctly. Associate Professor at ITU, Marco Carbone, has just received a grant from Independent Research Fund Denmark to that very purpose. In his research project, entitled “MECHANIsation of Session Types,” he is working on developing mathematical models that accurately represent software in order to detect flaws and errors. The project is specifically focused on distributed programs—software that runs parallel on multiple devices and machines—and the process of internal communication.

- A mathematical representation of a piece of software is much like an engineer’s schematics of a building. You start by calculating a model to ensure that the building, or in this case your piece of software, will not collapse, says Marco Carbone.

No human error

And there is a great need for better flaw detection in software. It used to be that the only way to test software was by taking a manual approach, testing for various problems the programmer could think of, but there is an infinite number of ways that any piece of software can be tested, and according to Marco Carbone there is a need for a more formalised approach. In his project, he looks at how software components interact through the lens of session types, a theoretical approach to categorising communication within software.

- If you have two elements in a piece of software communicating, you want to specify how they exchange information. If your software respects the session type parameters, it will run correctly. The problem is that all the models for how to evaluate this process only exist in hardcopy form and they are typically 50-100 pages long. So, what if a programmer makes a typo when implementing a proof model? It is roughly equivalent to a bricklayer laying down two bricks in a wall where he is only supposed to lay one, says Marco Carbone.

By using a so-called proof assistant that mechanises the evaluation of session type parameters, Marco Carbone hopes to help pave the way for better quality software in the future. The idea is to go from pen-and-paper mathematical proofs to machine-checked proofs, which will then pave the way for machine-checked integration in existing programming languages used for software development. The grant from Independent Research Fund Denmark means that he can hire a PhD-student to continue the work and extend on the current theories he has developed over the years of working in the field.

- At this point, my research is very much on the theoretical level, but I do see myself applying it practically in the future. Most people do not think about this often, but so many things in society and in our lives depends on software executing correctly. Ensuring a high quality of software is of the utmost importance.