Mattias Ulbrich

Dr. rer. nat. Mattias Ulbrich

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

ulbrich@kit.edu
Am Fasanengarten 5
Gebäude 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)

I am also interested in

  • Intermediate Verification Languages and Interaction
  • Dynamic Logic

Projects

IMPROVE APS
JML Standard

Committees

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

2017
Title Author(s) Source
Automating Regression Verification of Pointer Programs by Predicate AbstractionVladimir Klebanov
Philipp Rümmer
Mattias Ulbrich
Journal on Formal Methods in System Design
Proving JDK's Dual Pivot Quicksort CorrectBernhard Beckert
Jonas Schiffl
Peter H. Schmitt
Mattias Ulbrich
9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2017)
SemSlice: Exploiting Relational Verification for Automatic Program SlicingBernhard Beckert
Thorsten Bormer
Stephan Gocht
Mihai Herda
Daniel Lentzsch
Mattias Ulbrich
13th International Conference on integrated Formal Methods (iFM 2017)
Generalised Test Tables: A Practical Specification Language for Reactive SystemsBernhard Beckert
Suhyun Cha
Mattias Ulbrich
Birgit Vogel‑Heuser
Alexander Weigl
13th International Conference on integrated Formal Methods (iFM 2017)
Generation of Monitoring Functions in Production Automation Using Test SpecificationsSuhyun Cha
Sebastian Ulewicz
Birgit Vogel‑Heuser
Alexander Weigl
Mattias Ulbrich
Bernhard Beckert
15th IEEE International Conference on Industrial Informatics (INDIN 2017)
Generalized Test Tables: A Powerful and Intuitive Specification Language for Reactive SystemsAlexander Weigl
Franziska Wiebe
Mattias Ulbrich
Sebastian Ulewicz
Suhyun Cha
Michael Kirsten
Bernhard Beckert
Birgit Vogel‑Heuser
15th IEEE International Conference on Industrial Informatics (INDIN 2017)
2016
Title Author(s) Source
Deductive Software Verification - The KeY Book: From Theory to PracticeWolfgang Ahrendt
Bernhard Beckert
Richard Bubel
Reiner Hähnle
Peter H. Schmitt
Mattias Ulbrich
Lecture Notes in Computer Science 10001 (Springer 2016)
From Specification to Proof ObligationsDaniel Grahl
Mattias Ulbrich
Deductive Software Verification - The KeY Book: From Theory to Practice

Click here for a full list of my publications.

 

Supervised Theses

Title Year Type
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.
Generating Bounded Counterexamples for KeY Proof Obligations 2014 M.Sc.
Automating Regression Verification 2014 PdF
Proving Well-Definedness of JML Specifications with KeY 2013 M.Sc.
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
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