The Applied Formal Methods group investigates practical approaches to software modelling, verification and validation. The group aim is to apply and advance methods and tools that support modelling and verification of software-intensive systems. The research considers notation, methodology and tool development strongly intertwined, working towards practical tools for developing software suitable for use in critical systems. Such systems are mostly embedded control applications.

Software modelling differs from programming as the main interest is to arrive at descriptions of correct software with respect to properties required from it. In order to achieve this, software is considered as part of a system and the required properties span the software and its enclosing system. The methods to analyse formal models of software include proof, model checking, and animation. A specific challenge we address is to reduce the complexity of the required interactions with supporting tools.