Mattias Ulbrich

Dr. Mattias Ulbrich

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

ulbrich@kit.edu

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

Interests

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.

Projects

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

Committees

  • 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

Tools

  • 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

2021
Title Author(s) Source
Deductive Verification of Floating-Point Java Programs in KeYRosa Abbasi
Jonas Schiffl
Eva Darulova
Mattias Ulbrich
Wolfgang Ahrendt
Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II
Runtime Verification of Generalized Test TablesAlexander Weigl
Mattias Ulbrich
Shmuel S. Tyszberowicz
Jonas Klamroth
NASA Formal Methods - 13th International Symposium, NFM 2021, Virtual Event, May 24-28, 2021, Proceedings
Table-based formal specification approaches for control engineers—empirical studies of usabilitySuhyun Cha
Birgit Vogel‑Heuser
Alexander Weigl
Mattias Ulbrich
Bernhard Beckert
IET Cyber-Physical Systems: Theory and Applications
2020
Title Author(s) Source
Relational Test Tables: A Practical Specification Language for Evolution and SecurityAlexander Weigl
Mattias Ulbrich
Suhyun Cha
Bernhard Beckert
Birgit Vogel‑Heuser
FormaliSE@ICSE 2020: 8th International Conference on Formal Methods in Software Engineering, Seoul, Republic of Korea, July 13, 2020
Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeYWolfgang Ahrendt
Bernhard Beckert
Richard Bubel
Reiner Hähnle
Mattias Ulbrich
Lecture Notes in Computer Science 12345 (Springer 2020)
The VerifyThis Collaborative Long Term ChallengeMarieke Huisman
Raúl Monti
Mattias Ulbrich
Alexander Weigl
Deductive Software Verification: Future Perspectives: Reflections on the Occasion of 20 Years of KeY, Part IV: Feasibility and Usability
Usability Recommendations for User Guidance in Deductive Program VerificationSarah Grebing
Mattias Ulbrich
Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY, Part IV: Feasibility and Usability
Modular Verification of JML Contracts Using Bounded Model CheckingBernhard Beckert
Michael Kirsten
Jonas Klamroth
Mattias Ulbrich
9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2020), Part I: Verification Principles

Click here for a full list of my publications.

 

Supervised Theses

Title Year Type
Reconstructing Z3 Proofs With KeY 2021 M. Sc.
Property Types in Java: Combining TypeSystems and Deductive Verification 2021 M. Sc.
Techniques for Synthesizing Preconditionsfor Floating-Point Functions 2021 M. Sc.
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

 

Teaching

Title Type
Betreuung
Lehrbeauftragter
Betreuung
Lehrbeauftragter
Betreuung
VL-Vertretungen
Lehrbeauftragter
Betreuung
VL-Vertretungen
Lehrbeauftragter
VL-Vertretungen
Lehrbeauftragter
Übung zur Vorlesung
Lehrbeauftragter
Proseminar
Übung zur Vorlesung
Übung zur Vorlesung
Übung zur Vorlesung
Übung zur Vorlesung
Praktikum
Seminar
Praktikum
Seminar
Übung zur Vorlesung
Seminar
Übung zur Vorlesung
Click here to show all teaching activities