In our daily lives we are getting more and more dependent on IT-systems. We find them in embedded systems (like airplanes and medical equipment) and service-oriented systems (in for example the financial sector) and there is a move towards even more complex systems.
In cyber-physical systems the IT-systems interact with physical devices. This is taken even further in the ICT-powered systems of systems where several systems – including human processes – interact with one another. It is crucial that that these systems are reliable. They must be safe and secure and have acceptable performance properties.
In the section for Formal Methods we study techniques and tools that can make it possible to achieve these goals. We develop approaches for modelling systems and their properties; we push the state-of-the-art within analysis techniques for validating the properties of interest; and we investigate techniques for the realisation or implementation of the systems.
Our key competences are within program analysis (abstract interpretation and type systems), model checking (in discrete and stochastic variants), security (access control and protocol analysis) and software tools (compilers and abstract machines).