Home  |  Legals  |  Data Protection  |  Sitemap  |  KIT
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

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

2018
Title Author(s) Source
Proving Equivalence Between Imperative and MapReduce Implementations Using Program TransformationsBernhard Beckert
Timo Bingmann
Moritz Kiefer
Peter Sanders
Mattias Ulbrich
Alexander Weigl		rm Proceedings Third Workshop on Models for Formal Analysis of Real Systems rm and Sixth International Workshop on Verification and Program Transformation, rm Thessaloniki, Greece, 20th April 2018
2017
Title Author(s) Source
VerifyThis 2017: A Program Verification CompetitionMarieke Huisman
Rosemary Monahan
Wojciech Mostowski
Peter Müller
Mattias Ulbrich		Karlsruhe Institute of Technology 2017,10
An Interaction Concept for Program Verification Systems with Explicit Proof ObjectBernhard Beckert
Sarah Grebing
Mattias Ulbrich		Hardware and Software: Verification and Testing - 13th Haifa Verification Conference (HVC 2017)
Relational Program Reasoning Using Compiler IR – Combining Static Verification and Dynamic AnalysisMoritz Kiefer
Vladimir Klebanov
Mattias Ulbrich		Journal of Automated Reasoning
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)

Click here for a full list of my publications.

 

Supervised Theses

Title Year Type
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.
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.
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
Formale Systeme II: Theorie (SS 18) Lehrbeauftragter
Teamprojekt Lehramt Informatik (WS 17/18) Betreuung
Formale Systeme (WS 17/18) VL-Vertretungen
Formale Systeme II: Anwendung (SS 17) Lehrbeauftragter
Formale Systeme (WS 16/17) VL-Vertretungen
Formale Systeme II: Theorie (SS 16) Lehrbeauftragter
Formale Systeme (WS 15/16) Übung zur Vorlesung
Anwendung Formaler Verifikation (SS 15) Lehrbeauftragter
Desaster in der Software-Sicherheit (WS 14/15) Proseminar
Formale Systeme (WS 14/15) Übung zur Vorlesung
Formale Systeme (WS 13/14) Übung zur Vorlesung
Formale Systeme (WS 12/13) Übung zur Vorlesung
Formale Systeme (WS 11/12) Übung zur Vorlesung
Formale Entwicklung objektorientierter Software (WS 10/11) Praktikum
Formale Programmentwicklung (SS 10) Seminar
Formale Entwicklung objektorientierter Software (WS 09/10) Praktikum
Formale Programmentwicklung (SS 09) Seminar
Formale Systeme (WS 08/09) Übung zur Vorlesung
Formale Software-Entwicklung (SS 08) Seminar
Formale Systeme (WS 07/08) Übung zur Vorlesung
Click here to show all teaching activities
to top