From a research project to a software startup in Austria

We’re all about software bugs – from the mobile app which suddenly crashes, to the graphics card that cannot be handled by the operating system. We have almost become accustomed to the fact that computers are sometimes insecure, unpredictable and error-prone. But that does not have to be the case.

Prof. Laura Kovacs of the Institute of Logic and Computation of the Vienna University of Technology is developing methods to make our software safer and more reliable. In 2014 she was awarded an ERC Starting Grant of the European Research Council (ERC). Now, her research achievements have been rewarded with another ERC grant: Laura Kovacs will use her research results in industrial applications with the help of an ERC Proof of Concept grant. The foundation of an own start-up company is already planned. “We hope that within two years, we have implemented concrete programmes for commercialising our research.”

Set up by the European Union in 2011, the “Proof of Concept” grant by the ERC is funding researchers to explore the commercial or innovation potential of their research results. “Proof of Concept” grants are worth up to € 150,000 each and will be granted for excellent frontier research like Laura Kovacs’ work on automated assertion generation and automated theorem proving. 

More software, more mistakes

More and more aspects of our everyday life are regulated by software. In the past we have went to the bank counter, today we use online banking. Earlier, the phone was connected to the landline, today we need algorithms, to connect the mobile phone to the signal station. “The software is becoming more and more extensive and versatile, but its reliability does not increase,” says Laura Kovacs. “We are still working with software that is prone to errors and has security vulnerabilities.” 

The more complex our computer programs become, the more difficult it becomes for humans to understand them und to check them for errors. Today, therefore, attempts are being made to develop computer programs that can automatically detect errors in other computer programs. To achieve the goal of error-free, accurate software, the researchers are using the methods of formal logic. Laura Kovacs and her team have developed and improved such logical procedures in her ERC “Starting grant” project. “You can formally describe software in the language of mathematics and then prove that computer code has certain characteristics,” explains Kovacs. “Then you no longer have to hope that the program will deliver the right results in the future. You are able to prove with mathematical accuracy that in all situations the program will fulfill expected objectives.”

The new methods for automatic software validation are in comparison with other methods proving to be a great leap forward in many aspects. That is the main finding of practical tests on real computer code used in the industry done by the Laura Kovacs´s research group. “If a human being would need to develop similar proofs, that would be extremely time-consuming,” says Kovacs. “Our logic methods have already succeeded mathematically ensuring the expected behavior of the software in 80% of the cases.” 

The step towards the industry

The theoretical findings are now to be applied industrially. The European Research Council ERC is now supporting this step with another grant – the “proof of concept” grant. Laura Kovacs now wants to set up her own start-up company after analyzing the market and even better adapting the concepts to the requirements of industrial practice. “The long-term goal is to use logic in the software industry to find software errors and reliably correct them,” says Laura Kovacs. “We hope that within two years, we have implemented concrete programmes for commercialising our research, since we want the big companies to apply our method.”

German version of the text on the TU Wien website