Everything had been fine the day before, but on 19 July 2024, chaos suddenly reigned: millions of computers around the world went down, including important systems at hospitals, banks and airports. This incident went down in history as the ‘crowdstrike computer outage’. The reason was a software update that contained an insidious logic error.

It should be possible to prevent such disasters in the future - with the help of new logic methods that Prof Laura Kovacs and her team at the Institute of Logic and Computation at TU Wien have developed in their previous ERC project. She has now been awarded a ‘Proof of Concept Grant’ from the European Research Council (ERC), which will be used to develop LEARN - an interface that will make the logic tools already developed easier to use and deploy in the software industry.

Grant number four

ERC grants are the most highly endowed grants in the European research landscape. Winning such a grant is considered a great honour for excellent scientific work. Laura Kovacs, however, has not only received one, but now a total of four ERC grants: An ERC Starting Grant 2014 was followed by a Proof of Concept Grant, and her ERC Consolidator Grant 2020 has now been followed by another Proof of Concept Grant.

The Proof of Concept Grants are intended to put the scientific results of a successfully completed ERC Grant into practice, for example by developing a commercially marketable product.

Guaranteed correctness

Software has long since become so complex that individual people can no longer maintain a complete overview. Errors such as the crowdstrike update can therefore not be avoided even with careful maintenance. However, finding errors can be automated: Laura Kovacs is working on logic-based methods that can analyse existing software and guarantee absolute freedom from errors.

Doing numerical calculations has long been done much more efficiently by machines than by humans. Even symbolic calculations, such as transforming and solving equations, are no longer a problem for computers. A more recent development is that it is now also possible for machines to derive mathematical proofs automatically: Does a certain statement follow logically from certain other statements? Is it possible to show that a certain statement (or a list of statements) is always true, or is there a counterexample that nobody has thought of yet?

Such logic methods can be applied not only to mathematical statements, but also to computer programmes: Is the software error-free? Which properties of the software can be guaranteed with mathematical certainty? Is it possible to prove that the software provides the correct answer under all logically possible conditions?

Software tools of this kind have already been developed by Laura Kovacs' team. Now, as part of the proof-of-concept project, an interface called LEARN is to be created that makes these methods accessible in a simple and easy-to-learn way.

Great interest from the software industry

”This way, LEARN will be able to save huge costs that are incurred time and again for correcting faulty software updates,” says Laura Kovacs. “LEARN focuses on two things: Firstly, people working in software development can use it to learn logical modelling. Even for those who have little experience in this area, LEARN should be easy to use thanks to a simple, interactive interface. Secondly, LEARN independently develops proof strategies to guarantee the security of the system.”

The Proof of Concept Grant is endowed with €150,000 over a project period of 1.5 years. The product will be used in industrial environments - world-renowned companies such as Amazon, Certora and Microsoft have already signed up as early adopters. LEARN will also play a visible role in teaching: Hundreds of students at TU Wien will have the opportunity to use the tool to improve their logic and software analysis skills.

Contact

Prof. Laura Kovacs
Institute for Logic and Computation
TU Wien
+43 1 58801 18430
laura.kovacs@tuwien.ac.at