In software systems, errors may have catastrophic consequences, especially in systems that are critical for security, such as medical or aerospace programmes. Code checks and reviews may reduce the error rate, but in some cases, a higher security level is required. With this purpose, the formal methods form part of a category of techniques that analyse a mathematical description of the system in order to guarantee its accuracy. Some of the techniques used for formal software verification are model checking, theorem demonstration and static analysis. One problem that all these methods share is the high degree of computational complexity, which may limit applicability in real-world examples. This line of research takes pragmatic approaches into account in order to guarantee the software systems' quality on an industrial scale, and explores key topics such as usability, efficiency and applicability.
