The Institute for Formal Models and Verification (FMV), led by Prof. Bernhard Aichernig, specializes in the research and application of formal methods for software development. Formal methods are mathematically rigorous techniques and tools used for the specification, design, and verification of software and hardware systems.

Our work spans all phases of development — from requirements engineering, through testing and verification, to reverse engineering. The overarching goal is to demonstrate that a system behaves correctly under all possible conditions. Most recently, we have extended our research to investigate the dependability of AI systems.

Our research activities are organized into the following categories:
    • Specification & Design focuses on the early phases of development, aiming to find suitable abstractions and formalizations for complex problems.
    • Automata Learning develops methods and tools for automatically learning formal models from data (passive learning) or through interaction with a system (active learning), enabling the analysis of systems without requiring internal access.
    • Falsification addresses software testing, providing methods such as automated test-case generation to efficiently uncover defects and weaknesses.
    • Verification seeks to prove that a software system or component is free of flaws. Techniques like proof-based development enable the creation of software that is correct by design.

Our group combines a strong theoretical background in formal methods with practical applications across various industries, including the automotive domain.