Mattias Ulbrich

Dr. Mattias Ulbrich is a Research Fellow at the Institute of Information Security and Dependability (KASTEL) within the Department of Informatics at Karlsruhe Institute of Technology (KIT). His primary research focus lies in formal deductive software verification at the program code level, with special emphasis on relational verification where multiple programs are considered simultaneously. His work spans regression verification, equivalence checking, algorithm refinement, and verification of relational properties of algorithms.

His research interests include formal software verification, relational verification techniques, program equivalence checking, information flow security, and intermediate verification languages. Ulbrich has made significant contributions to the KeY project, an integrated deductive software design tool, and has developed various verification tools including rêve for program equivalence checking and SemSlice for precise program slicing. His work bridges theoretical foundations with practical applications in software verification.

Analysis of his recent publications reveals a strong trend toward practical applications of formal verification methods, particularly in industrial contexts like automated production systems. His work increasingly focuses on usability of verification tools, integration of different verification paradigms, and application to real-world software systems including JDK components. There's also growing interest in educational aspects of formal methods, as seen in his work on introducing algorithmic thinking to younger students.

Ulbrich has supervised numerous Master's and Bachelor's theses across a wide range of verification topics, demonstrating his commitment to mentoring the next generation of formal methods researchers. His teaching activities include courses on formal systems and verification at KIT, with particular focus on teacher education programs in computer science.

He is actively involved in the formal methods community, serving on program committees for major conferences including VSTTE, VerifyThis, and ISoLA. Ulbrich has been a steering committee member for VerifyThis since 2019 and has co-organized several workshops and Dagstuhl seminars focused on program equivalence and relational verification.