Using mathematics to hunt for computer errors

Improving the security of computer software and hardware requires mathematical analytic methods. Thanks to research by a team of computer scientists led by Krishnendu Chatterjee in a project funded by the Austrian Science Fund FWF, these methods will work significantly faster in the future.

Security gap in application discovered, update urgently recommended. Alerts like that can confront us every week. Often, a comprehensive update that addresses teething troubles is already offered when a new programme is launched. This creates manifold problems, and public entities as well as businesses are often exposed to attacks by hackers. Software is used in a growing number of sensitive areas where a computer failure might even be life threatening. It has to be noted that not all fields are affected in the same way, many computer systems run as unfailingly as the proverbial Swiss clockwork. While hardware is usually very reliable, it is the software component that may create problems.

Mathematics improve computer systems
Complex programmes actually make it very difficult to foresee every eventuality. While computer methods for testing software exist, the complexity of applications has been steadily increasing in recent years. The performance of test methods lags behind, particularly in terms of their speed – a good incentive to invest in basic research in this field. In a recently completed project funded by the Austrian Science Fund FWF, the computer scientist Krishnendu Chatterjee analysed computer systems with the help of mathematical methods with hope of providing significant improvements in this sector.

Graph theory
"This field has a long-standing tradition", says Chatterjee. "Researchers have long been trying to find a formal basis for designing correct systems. Fundamental developments in this area go back to the 1960s, like the work by Alonzo Church, one of the founding fathers of computer sciences." For the mathematical analysis of computer systems, scientists use what is called 'graph theory', which deals with objects that can be characterised as networks of interconnected points or vertices. Computer systems can be mathematically described as graphs, with a vertex representing a certain state of the system and an edge representing a transition between two states. A computer displaying this text, for instance, is in a defined state represented as a vertex. When the user clicks on a link, the system changes to another state, and this transition is shown as an edge.

Improved graph algorithms
This method is particularly suited for the verification of computer systems. Chatterjee was interested in how fast these verification algorithms work. "Computer systems are getting more complex all the time", the computer scientist notes. "In some algorithmic problems in verification development has been stagnating since the 1990s. A new aspect of this project was to use cutting-edge approaches from graph theory to improve the algorithms. That was a completely new line of attack." Chatterjee emphasises the significance of his cooperation with his project partner Monika Henzinger from the University of Vienna. "For me, that was an intensive learning process. It was intriguing to see how the methods of graph algorithms need to be adapted and expanded in order to arrive at better algorithms for the problems we studied."

Limits, conditions, successes
In that respect, the project was very successful: several speed limits for certain verification algorithms were broken for the first time since the 1990s, for instance involving so-called 'Markov decision processes', which are models containing several options and an element of randomness. "One example for that would be the development of robots", explains Chatterjee. "A robot interacts with an environment which includes uncertainties and it has several options, such as veering to the left or to the right. Markov decision processes provide a model for that." For many applications it is essential to predict in such a model what events will occur with certainty. "The most efficient algorithm for addressing that problem available till now dated back to 1995 and had quadratic complexity", notes Chatterjee. This means that the runtime of the algorithm increases quadratically with the size of the system being verified – hence, a system double in size requires fourfold runtime. "In our project we were able to overcome this limit by using graph algorithm techniques."

Chatterjee is very pleased with the success of the project. "Our two doctoral students, Sebastian Krinninger and Martin Chmelik, also did excellent work, both received prizes for their dissertations", notes Chatterjee. Despite the topical relevance of the subject he underlines that his was a pure basic research project. "Our first project was very theoretical. Now we are trying to explore limits or conditions to see how hard it is going to be to improve our algorithms further. At the same time we want to see how these approaches can be translated into practice."

FWF Austrian Science Fund

The Austrian Science Fund (FWF) is Austria's central funding organization for basic research.

The purpose of the FWF is to support the ongoing development of Austrian science and basic research at a high international level. In this way, the FWF makes a significant contribution to cultural development, to the advancement of our knowledge-based society, and thus to the creation of value and wealth in Austria.

Scientific Contact
Prof. Krishnendu Chatterjee
IST Austria
Am Campus 1
A-3400 Klosterneuburg
T +43 / 2243 / 9000 3201
E Krishnendu.Chatterjee@ist.ac.at
W https://ist.ac.at/

Austrian Science Fund FWF
Ingrid Ladner
Haus der Forschung
Sensengasse 1
1090 Vienna, Austria
T +43 / 1 / 505 67 40 - 8111
E ingrid.ladner@fwf.ac.at
W http://scilog.fwf.ac.at
W http://www.fwf.ac.at

Distribution
PR&D – Public Relations for Research and Education
Mariannengasse 8
1090 Vienna, Austria
T +43 / 1 / 505 70 44
E contact@prd.at
W http://www.prd.at/en

This release was published on openPR.