We all get frustrated with software faults - from mobile phones that suddenly crash, to graphics cards that are not compatible with our new operating system. We have almost become used to the idea that computers are sometimes unstable, unpredictable and prone to error. But it doesn't have to be like that.

Professor Laura Kovacs from the Institute of Logic and Computation at TU Wien is developing methods to make our software more stable and more reliable. In 2014, she was awarded an ERC Starting Grant by the European Research Council. She has now received further ERC funding as a result of her research success: with the support of an ERC Proof of Concept grant, Laura Kovacs is now seeking to introduce her findings into industrial applications. She already has plans to establish her own start-up business.

More software, more errors

More and more aspects of our everyday life are governed by software. In the old days we paid a visit to the bank, these days we use online banking. Our telephone used to be connected to a landline network, now we need algorithms, such as those enabling mobile phone signals to move from one transmission station to another. "Software is becoming increasingly extensive and versatile, but its reliability is not improving," says Laura Kovacs. "We continue to work with software that is prone to error and has security loopholes."

The more complex computer programs become, the more difficult it becomes for people to understand them and search for faults. We are therefore now trying to develop computer programs that can detect faults in other computer programs automatically. To move closer towards our objective of error-free, secure software, we need to make use of formal logic methods. As part of her ERC project, Laura Kovacs and her team have managed to develop and improve these kinds of logical processes.

"We can describe software formally in the language of mathematics and then prove that the computer code has certain properties," explains Kovacs. "Then, we no longer need to simply hope that the program will continue to provide the right outputs in future – we can demonstrate with mathematical certainty that these requirements will be fulfilled in any situation."

The new methods for the automatic verification of software are considered to be different in key aspects from previously used methods - such as is evidenced by practical tests in which the new concepts conceived by Laura Kovacs' working group are applied to real computer codes from industry. "If we used people to provide similar evidence, it would be extremely time consuming," says Kovacs. "But our logic methods have already demonstrated that the anticipated behaviour of software can be mathematically guaranteed in 80% of cases."

From theory to practice

The theoretical findings now need to be applied in industry. This step is now being supported by the European Research Council (ERC) in the form of additional funding - the Proof of Concept grant. After analysing the market and further modifying her concepts to the requirements of industry in practice, Laura Kovacs now wants to set up her own start-up business. "The long-term objective is to introduce logic into the software industry to find software faults and reliably correct them," says Laura Kovacs.

Foto: Luiza Puiu