Home | Legals | Sitemap | KIT
Mattias Ulbrich

Dr. rer. nat. Mattias Ulbrich

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

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

K e Y


The KeY Project
 

IMPROVE
IMPROVE
(DFG-SPP1593: Design for Future - Managed Software Evolution)

Tools

  • rêve - Automatically check two programs for equivalence
  • TABLET - 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

Publications
Mattias Ulbrich, Luzie Schreiter, Sarah Grebing, Jörg Raczkowsky, Heinz Wörn and Bernhard Beckert.
A Concept for Multi-Phase Incremental Formal Verification in Robotic Guided Surgery
In 4th International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS)
2015
(Work-in-progress Paper. To appear)
Sebastian Ulewicz, Mattias Ulbrich, Alexander Weigl, Bernhard Beckert and Birgit Vogel-Heuser.
Proving Equivalence between Control Software Variants for Programmable Logic Controllers - Using Regression Verification to Reduce Unneeded Variant Diversity
In ETFA2015
2015
(To appear)
Bernhard Beckert, Mattias Ulbrich, Birgit Vogel-Heuser and Alexander Weigl.
Regression Verification for Programmable Logic Controller Software
In 17th International Conference on Formal Engineering Methods (ICFEM 2015)
LNCS 9407, Springer, 2015
Vladimir Klebanov, Mattias Ulbrich Bernhard Beckert.
Regression Verification for Java Using a Secure Information Flow Calculus
In 17th Workshop on Formal Techniques for Java-like Programs (FTfJP 2015)
2015
Peter H. Schmitt and Mattias Ulbrich.
Axiomatization of Typed First-Order Logic
In 20th International Symposium on Formal Methods (FM 2015)
LNCS 9109, 2015
Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer and Mattias Ulbrich.
Automating Regression Verification
In Multikonferenz Software Engineering und Management 2015
LNI, 2015
(To appear)
Wojciech Mostowski and Mattias Ulbrich.
Dynamic Dispatch for Method Contracts through Abstract Predicates
In 15th International Conference on MODULARITY (MODULARITY15)
ACM, 2015
(To appear)
Wolfgang Ahrendt, Bernhard Beckert, Daniel Bruns, Richard Bubel, Christoph Gladisch, Sarah Grebing, Reiner Hähnle, Martin Hentschel, Mihai Herda, Vladimir Klebanov, Wojciech Mostowski, Christoph Scheben, Peter H. Schmitt and Mattias Ulbrich.
The KeY Platform for Verification and Analysis of Java Programs
In Verified Software: Theories, Tools, and Experiments (VSTTE 2014)
LNCS 8471, Springer, 2014
Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer and Mattias Ulbrich.
Automating Regression Verification
In 29th IEEE/ACM International Conference on Automated Software Engineering (ASE 2014)
ASE '14, ACM, 2014
Aboubakr Achraf El Ghazi, Mattias Ulbrich, Christoph Gladisch, Shmuel Tyszberowicz and Mana Taghdiri.
JKelloy: A Proof Assistant for Relational Specifications of Java Programs
In 6th NASA Formal Methods Symposium (NFM 2014)
LNCS 8430, Springer, 2014
Bernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt and Mattias Ulbrich.
Information Flow in Object-Oriented Software
In 23rd International Symposium on Logic-Based Program Synthesis and Transformation, (LOPSTR 2013)
Dpto. de Systemas Informáticos y Computation, Universidad Complutense de Madrid, TR-11-13, 2013
Daniel Bruns, Wojciech Mostowski and Mattias Ulbrich.
Implementation-level verification of algorithms with KeY
International Journal on Software Tools for Technology Transfer (STTT) 17(6):729-744
Springer, 2013
Mattias Ulbrich, Mana Taghdiri Aboubakr Achraf El Ghazi and Mihai Herda.
Reducing the Complexity of Quantified Formulas via Variable Elimination
In 11th International Workshop on Satisfiability Modulo Theories (SMT)
2013
Mattias Ulbrich.
Dynamic Logic for an Intermediate Language: Verification, Interaction and Refinement
Doctoral dissertation.
Karlsruhe Institute of Technology, 2013
Mattias Ulbrich, Ulrich Geilmann and Aboubakr Achraf El Ghazi and Mana Taghdiri.
A Proof Assistant for Alloy Specifications
In 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
LNCS 7214, Springer, 2012
Ulrich Geilmann, Mattias Ulbrich Aboubakr Achraf El Ghazi and Mana Taghdiri.
A Dual-Engine for Early Analysis of Critical Systems
In Workshop on Dependable Software for Critical Infrastructures (DSCI)
2011
Peter H. Schmitt, Mattias Ulbrich and Benjamin Weiß.
Dynamic Frames in Java Dynamic Logic
In Revised Selected Papers, International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010)
LNCS 6528, Springer, 2011
Mattias Ulbrich.
A Dynamic Logic for Unstructured Programs with Embedded Assertions
In Revised Selected Papers, International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010)
LNCS 6528, Springer, 2011
(This paper has been awarded the best student paper and presentation award.)
Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan and Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans and Stephan Tobies, Thomas Tuerk, Mattias Ulbrich and Benjamin Weiß.
The 1st Verified Software Competition: Experience Report
In Proceedings, 17th International Symposium on Formal Methods (FM 2011)
LNCS 6664, Springer, 2011
Roman Krenický and Mattias Ulbrich.
Deductive Verification of a Byzantine Agreement Protocol
Technical report.
Karlsruhe Institute of Technology, Department of Informatics (2010-7), 2010
Peter H. Schmitt, Mattias Ulbrich and Benjamin Weiß.
Dynamic Frames in Java Dynamic Logic: Formalisation and Proofs
Technical report.
Department of Computer Science, Karlsruhe Institute of Technology (2010-11), 2010
Mattias Ulbrich.
Software Verification for Java 5
Diplomarbeit, Fakultät für Informatik, Universität Karlsruhe, 2007
(This thesis has been awarded the Förderpreis ObjektForum 2007)
Mattias Ulbrich.
Bereitstellung und Zuweisung von Ressourcen in der formalen algorithmischen Synthese
Studienarbeit, Fakultät für Informatik, Universität Karlsruhe, 2005

Teaching
Title Type
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