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

Publications

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
Modular Specification and VerificationDaniel Grahl
Richard Bubel
Wojciech Mostowski
Peter H. Schmitt
Mattias Ulbrich
Benjamin Weiß
Deductive Software Verification - The KeY Book: From Theory to Practice
Proof Search with TacletsPhilipp Rümmer
Mattias Ulbrich
Deductive Software Verification - The KeY Book: From Theory to Practice
Dynamic Dispatch for Method Contracts through Abstract PredicatesWojciech Mostowski
Mattias Ulbrich
Transactions on Modularity and Compoisition 1
Relational Program Reasoning Using Compiler IRMoritz Kiefer
Vladimir Klebanov
Mattias Ulbrich
Verified Software. Theories, Tools, and Experiments - 8th International Conference, VSTTE 2016, Revised Selected Papers
Automated Verification for Functional and Relational Properties of Voting RulesBernhard Beckert
Thorsten Bormer
Michael Kirsten
Till Neuber
Mattias Ulbrich
Sixth International Workshop on Computational Social Choice (COMSOC 2016)
A Verification-Supported Evolution Approach to Assist Software Application Engineers in Industrial Factory AutomationSebastian Ulewicz
Mattias Ulbrich
Alexander Weigl
Michael Kirsten
Franziska Wiebe
Bernhard Beckert
Birgit Vogel‑Heuser
IEEE International Symposium on Assembly and Manufacturing (ISAM), Fort Worth, USA
2015
Title Author(s) Source
A Concept for Multi-Phase Incremental Formal Verification in Robotic Guided SurgeryMattias Ulbrich
Luzie Schreiter
Sarah Grebing
Jörg Raczkowsky
Heinz Wörn
Bernhard Beckert
4th International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS)
Proving Equivalence between Control Software Variants for Programmable Logic Controllers - Using Regression Verification to Reduce Unneeded Variant DiversitySebastian Ulewicz
Mattias Ulbrich
Alexander Weigl
Bernhard Beckert
Birgit Vogel‑Heuser
20th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2015)
Regression Verification for Programmable Logic Controller SoftwareBernhard Beckert
Mattias Ulbrich
Birgit Vogel‑Heuser
Alexander Weigl
17th International Conference on Formal Engineering Methods (ICFEM 2015)
Regression Verification for Java Using a Secure Information Flow CalculusBernhard Beckert
Vladimir Klebanov
Mattias Ulbrich
17th Workshop on Formal Techniques for Java-like Programs (FTfJP 2015)
Axiomatization of Typed First-Order LogicPeter H. Schmitt
Mattias Ulbrich
20th International Symposium on Formal Methods (FM 2015)
Automating Regression VerificationDennis Felsing
Sarah Grebing
Vladimir Klebanov
Philipp Rümmer
Mattias Ulbrich
Multikonferenz Software Engineering und Management 2015
Dynamic Dispatch for Method Contracts through Abstract PredicatesWojciech Mostowski
Mattias Ulbrich
14th International Conference on MODULARITY (MODULARITY15)
2014
Title Author(s) Source
The KeY Platform for Verification and Analysis of Java ProgramsWolfgang 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
Mattias Ulbrich
6th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2014)
Automating Regression VerificationDennis Felsing
Sarah Grebing
Vladimir Klebanov
Philipp Rümmer
Mattias Ulbrich
29th IEEE/ACM International Conference on Automated Software Engineering (ASE 2014)
JKelloy: A Proof Assistant for Relational Specifications of Java ProgramsAboubakr Achraf El Ghazi
Mattias Ulbrich
Christoph Gladisch
Shmuel Tyszberowicz
Mana Taghdiri
6th NASA Formal Methods Symposium (NFM 2014)
2013
Title Author(s) Source
Information Flow in Object-Oriented SoftwareBernhard Beckert
Daniel Bruns
Vladimir Klebanov
Christoph Scheben
Peter H. Schmitt
Mattias Ulbrich
23rd International Symposium on Logic-Based Program Synthesis and Transformation, (LOPSTR 2013)
Implementation-level verification of algorithms with KeYDaniel Bruns
Wojciech Mostowski
Mattias Ulbrich
International Journal on Software Tools for Technology Transfer (STTT) 17(6)
Reducing the Complexity of Quantified Formulas via Variable EliminationAboubakr Achraf El Ghazi
Mattias Ulbrich
Mana Taghdiri
Mihai Herda
11th International Workshop on Satisfiability Modulo Theories (SMT)
Dynamic Logic for an Intermediate Language: Verification, Interaction and RefinementMattias UlbrichKarlsruhe Institute of Technology (June 2013)
2012
Title Author(s) Source
A Proof Assistant for Alloy SpecificationsMattias Ulbrich
Ulrich Geilmann
Aboubakr Achraf El Ghazi
Mana Taghdiri
18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
2011
Title Author(s) Source
A Dual-Engine for Early Analysis of Critical SystemsAboubakr Achraf El Ghazi
Ulrich Geilmann
Mattias Ulbrich
Mana Taghdiri
Workshop on Dependable Software for Critical Infrastructures (DSCI)
Dynamic Frames in Java Dynamic LogicPeter H. Schmitt
Mattias Ulbrich
Benjamin Weiß
Revised Selected Papers, International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010)
A Dynamic Logic for Unstructured Programs with Embedded AssertionsMattias UlbrichRevised Selected Papers, International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010)
The 1st Verified Software Competition: Experience ReportVladimir 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ß
Proceedings, 17th International Symposium on Formal Methods (FM 2011)
2010
Title Author(s) Source
Deductive Verification of a Byzantine Agreement ProtocolRoman Krenický
Mattias Ulbrich
Karlsruhe Institute of Technology, Department of Informatics 2010-7
Dynamic Frames in Java Dynamic Logic: Formalisation and ProofsPeter H. Schmitt
Mattias Ulbrich
Benjamin Weiß
Department of Computer Science, Karlsruhe Institute of Technology 2010-11
2007
Title Author(s) Source
Software Verification for Java 5Mattias UlbrichFakultät für Informatik, Universität Karlsruhe (January 2007)
2005
Title Author(s) Source
Bereitstellung und Zuweisung von Ressourcen in der formalen algorithmischen SyntheseMattias UlbrichFakultät für Informatik, Universität Karlsruhe (January 2005)

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