Mattias Ulbrich

Dr. Mattias Ulbrich

Room: 229
Phone: +49 721 608-44338
Fax: +49 721 608-44021

[ S/MIME | GPG/Enigmail ]
Am Fasanengarten 5
Building 50.34
76131 Karlsruhe

Wintersemester 2022/2023

In den Wintersemestern 2022/2023 und 2023/2024 vertrete ich eine vakante Professur an der KIT-Fakultät für Informatik.

Für Fragen zur Vorlesung Grundbegriffe der Informatik können Sie sich an den Übungsleiter Philipp Kern oder mich wenden.


My research focuses on formal deductive software verification on the level of program code. I am particularly intersted in relational verification, i.e., cases where more than one program is considered for the verification:

  • Regression verification, equivalence checking
  • Algorithm Refinement
  • Verification of relational properties of algorithms
  • Information Flow Security (to a lesser extend)
  • Relational Properties of Software for Automated Production Systems

I am also interested in

  • Intermediate Verification Languages and Interaction
  • Dynamic Logic

Teacher Eduction

I am a contact person for the degree programme "Lehramt an Gymnasien - Teilstudiengang Informatik" (B.Ed./M.Ed/M.Ed.Erg.).

If you are a student with a question regarding the programme; or if you are interested in enrolling in the programme; feel free to contact me. Alternatively, you can contact the study service center Informatics.

I am coordinating the development for the installation of the teaching lab informatics at KIT.


K e Y
The KeY Project
(DFG-SPP1593: Design for Future - Managed Software Evolution)
Open-source Teaching Software Laboratory
JML Standard


  • PERR 2019, PC co-chair
  • Steering Committee VerifyThis (since 2019)
  • Dagstuhl 18-151, co-organiser
  • VSTTE 2018, PC member
  • PAAR 2018, PC member
  • MODELS (Tutorials) 2018, PC member
  • VSTTE 2017, PC member
  • VerifyThis 2017, Co-organiser
  • HFC 2017, PC member
  • JML Workshop Bad Herrenalb, 2016, Co-organiser
  • Peer reviewing for journals: TOPLAS, at, FMSD, STTT
  • lots of subreviewing


  • rêve - Automatically check two programs for equivalence
  • rêve for noninterference - Automatically prove noninterference of a C routine
  • SemSlice - Automatically semantic analysis for precise programs slicing
  • Tableau Applet - A Java Applet for a first tableau calculus (w/ some automation), mainly for teaching purposes
  • KeY - Integrated Deductive Software Design
  • ivil - Interactive Verification on Intermediate Language

Recent Publications

Title Author(s) Source
Formally Verifying an Efficient Sorter, extended versionBernhard Beckert
Peter Sanders
Mattias Ulbrich
Julian Wiesler
Sascha Witt
Title Author(s) Source
Formal Specification and Verification of JDK’s Identity Hash Map ImplementationMartin de Boer
Stijn de Gouw
Jonas Klamroth
Christian Jung
Mattias Ulbrich
Alexander Weigl
17th International Conference on integrated Formal Methods (iFM 2022)
The Karlsruhe Java Verification SuiteJonas Klamroth
Florian Lanzinger
Wolfram Pfeifer
Mattias Ulbrich
The Logic of Software. A Tasting Menu of Formal Methods: Essays Dedicated to Reiner Hähnle on the Occasion of His 60th Birthday
Inferring Interval-Valued Floating-Point PreconditionsJonas Krämer
Lionel Blatter
Eva Darulova
Mattias Ulbrich
28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022), held as part of ETAPS 2022: European Joint Conferences on Theory and Practice of Software, Part I
Title Author(s) Source
Design- and Evaluation-Concept for Teaching and Learning Laboratories in Informatics Teacher EducationBernhard Standl
Anette Bentz
Mattias Ulbrich
Annika Vielsack
Ingo Wagner
Informatics in Schools. Engaging Learners in Computational Thinking - 13th International Conference, ISSEP 2020, Tallinn, Estonia, November 16-18, 2020, Proceedings
Title Author(s) Source
Reconstructing Z3 proofs in KeY: There and back againWolfram Pfeifer
Jonas Schiffl
Mattias Ulbrich
Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs (FTfJP 2021), co-located with ECOOP/ISSTA 2021, Online, 13 July 2021
Scalability and Precision by Combining Expressive Type Systems and Deductive VerificationFlorian Lanzinger
Alexander Weigl
Mattias Ulbrich
Werner Dietl
Proceedings of the ACM on programming languages 5(OOPSLA)
Deductive Verification of Floating-Point Java Programs in KeYRosa Abbasi
Jonas Schiffl
Eva Darulova
Mattias Ulbrich
Wolfgang Ahrendt
27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021), held as part of ETAPS 2021: European Joint Conferences on Theory and Practice of Software, Part II

Click here for a full list of my publications.


Supervised Theses

Title Year Type
Cooperative Specification Extraction for KeY 2022
Generating Mutation Tests Using an Equivalence Prover 2022 PdF
Formal Specification and Verification of a Java Implementation of Super Scalar Sample Sort 2022 M. Sc.
Property Types for Mutable Data Structures in Java 2022 M. Sc.
A Formal Notion of Leakage Regression for Timed Automata 2022 B. Sc.
Specification and Verification of Hash Table Data Structures with KeY 2021 B. Sc.
Reconstructing Z3 Proofs With KeY 2021 M. Sc.
Property Types in Java: Combining TypeSystems and Deductive Verification 2021 M. Sc.
Techniques for Synthesizing Preconditions for Floating-Point Functions 2021 M. Sc.
Using Machine Learning to Improve Strategy Selection in KeY 2020 PdF
Modelling and Exploiting Ownership-Annotations Using Dynamic Frames in KeY 2020 B. Sc.
Ein Rahmenwerk für Experimente zur Evaluation der Verwendung digitaler Medien im Informatikunterricht 2020 M. Ed.
Specification and Verification of Java Programs with Lambda Expressions 2019 B. Sc.
Specification and Verification of the Arbitrary Precision Integer Multiplication in Java's BigInteger Class 2019 B. Sc.
Modular Verification of JML Contracts Using Bounded Model Checking 2019 M. Sc.
Runtime Monitoring of Event-driven Software Systems Specified Using Interface State Machines: Formal Semantics and Implementation 2018 M. Sc.
Comparing Deductive Program Verification of Graph Data-Structures 2018 B. Sc.
Automatic Relational Reasoning for Algebraic Data Types 2018 M. Sc.
Sampling-based Execution Coverage Estimation for Partially Proved Java Program Specifications 2018 M. Sc.
Evaluation der Proof-Script-Sprache für KeY 2018 B. Sc.
A Divide-and-Conquer Strategy with Block and Loop Contracts for Deductive Program Verification 2018 B. Sc.
Exploiting Runtime Data to Derive Formal Environment Models for the Verification of PLC Software 2017 B. Sc.
Relational Equivalence Proofs Between Imperative and MapReduce Algorithms 2017 PdF
Relational Verification of Floating-point Programs 2017 PdF
Exploiting Runtime Data to Derive Formal Environment Models for the Verification of PLC Software 2017 B. Sc.
Specifying and Verifying Real-World Java Code with KeY - Case Study java.math.BigInteger 2017 B. Sc.
Semantic Slicing 2016 PdF
Dynamic Analysis for Automatic Relational Verification 2016 B.Sc.
Dual Pivot Quicksort: Specification and Verification using KeY 2016 B.Sc.
Theory of Refinement of Cyber-Physical Systems into Implementations 2015 B.Sc.
Regression Verification for Programmable Logic Controller Software 2015 M.Sc.
Generating Bounded Counterexamples for KeY Proof Obligations 2014 M.Sc.
Automating Regression Verification 2014 PdF
Proving Well-Definedness of JML Specifications with KeY 2013 StA
Design and Implementation of a Verification Framework for Java Bytecode using Unstructured Dynamic Logic 2012 DA
Introducing the Boogie methodology to USDL 2011 StA
Verifying Alloy Models Using KeY 2011 DA
Funktionsabschlüsse in Dynamischer Logik 2010 StA
Formal Semantics for the Java Modeling Language 2009 DA
Click here to show all supervised theses
M/B.Sc.=Master/Bachelor, PdF=Praxis der Forschung, StA=Studienarbeit, DA=Diplomarbeit



Title Type
Übung zur Vorlesung
Übung zur Vorlesung
Übung zur Vorlesung
Übung zur Vorlesung
Übung zur Vorlesung
Übung zur Vorlesung
Übung zur Vorlesung
Click here to show all teaching activities