Formal methodes for the design and analysis of complex systems

Like mathematics, computer science deals with abstract objects. However, while mathematics deals with figures, shapes, relations, etc., computer science focuses on concepts such as algorithms and information. At the same time, computer science is an engineering discipline. Engineers design things: IT engineers design hardware and especially software. The objective of any engineering discipline is to transform the design process from an art - in which the result depends on individual talent - into a science with well-grounded methodology. When a construction engineer designs a bridge, he/she knows which calculations have to be carried out. In the end, the bridge will be able to withstand precisely those conditions the engineer calculated. However, computer science is a younger discipline than construction engineering, and the mathematical methods for predicting the properties of software systems have not yet fully matured. Once software is developed, it has to be tested, and software bugs are still a common occurrence. In addition, there is another fundamental difference between computer science and construction engineering: If you remove a single rivet from a (well-designed) bridge, it will not collapse right away. One minor error will not lead to immediate disaster. In the case of software, it is difficult to rule out such minor errors with serious consequences. Changing a single letter in a programme`s code can cause a computer to crash. The reason for this phenomenon is that software constitutes what is known as a discrete system. The purpose of Thomas A. Henzinger`s research is to develop algorithmic methods which improve the reliability of software. These methods rely on formal logic and mathematical theories to model and analyse discrete, dynamic systems. One especially difficult - and thus scientifically interesting - area is software systems which consist of many parts which communicate with one another. Another challenge can be found in the software used to control critical and often vitally important processes such as those executed in every modern automobile or pacemaker. For over ten years, Henzinger and his team have been developing fundamental mathematical models for process control software. At the Institute of Science and Technology (IST) Austria, computer scientists and biologists work together in an interdisciplinary environment. Specifically, their objective is to advance mathematical software modelling methods so that they can be used to analyse processes in living cells and organs. The ultimate goal of this research is to map a complete organism in the form of software. The Wittgenstein Award will help Henzinger and his team make further progress in these research efforts.

Formal methods can ensure the safety of hardware and software systems, but they can also be used to predict the behavior of complex systems in other domains, such as engineering, economics, and biology. In this project, we developed the following formal methods for the design and analysis of complex systems: (1) solving bidding games on graphs for the design and analysis of stateful auctions; (2) mining hybrid automaton models from time-series data for the modeling and analysis of mixed discrete-continuous systems; (3) model checking the evolution of gene regulatory networks; (4) stepwise refinement and structured verification of asynchronous concurrent programs; (5) learning biologically inspired neural network motifs for resilient and interpretable control applications; (6) identifying cost-precision trade-offs in the approximative monitoring of complex systems; (7) predicting the long-run behavior of probabilistic systems through runtime verification; (8) using abstract interpretation for novelty detection and online supervision of neural networks.