Home | deutsch | Legals | Sitemap | KIT
MattiasUlbrich

Dipl.-Inform. Mattias Ulbrich
Wiss. Mitarbeiter
Room: 106
Phone: +49 721 608-44338
Fax: +49 721 608-44211
mulbrichRbx9∂ira uka de
 Am Fasanengarten 5
Gebäude 50.34
D-76131 Karlsruhe

Interests

  • Abstract Formal Modelling and Specification
  • Intermediate Verification Languages and Interaction
  • Dynamic Logic
  • The Event-B Methodology

Project

K e Y
The KeY Project

Tools

I am involved in the development of:

  • 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

Notes

Publications
Title Author Source
A Proof Assistant for Alloy Specifications

Mattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi, Mana Taghdiri

18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2012
A Dual-Engine for Early Analysis of Critical Systems

Aboubakr Achraf El Ghazi, Ulrich Geilmann, Mattias Ulbrich, Mana Taghdiri

Dependable Software for Critical Infrastructures (DSCI), 2011
The 1st Verified Software Competition: Experience Report

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, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, Benjamin Weiß

17th International Symposium on Formal Methods (FM 2011), Limerick, Ireland. LNCS 6664, Springer, 2011. Best paper award at FM 2011.
A Dynamic Logic for Unstructured Programs with Embedded Assertions

Mattias Ulbrich

International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), Paris, France. LNCS 6528, Springer, 2011
Dynamic Frames in Java Dynamic Logic

Peter H. Schmitt
Mattias Ulbrich
Benjamin Weiß

International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), Paris, France. LNCS 6528, Springer, 2011
Deductive Verification of a Byzantine Agreement Protocol

Roman Krenický
Mattias Ulbrich

digital library of the KIT


Teaching
Title Type
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) lecture
Formale Software-Entwicklung (SS 08) Seminar
Formale Systeme (WS 07/08) Vorlesung


Diplom- / Studienarbeit
Titel Typ Datum: Betreuer:
Software Verification for Java 5 Diplomarbeit 2007

Prof. P.H. Schmitt
Richard Bubel
Steffen Schlager
Bereitstellung und Zuweisung von Ressourcen in der formalen algorithmischen Synthese Studienarbeit 2005

Dr. Kai Kapp