Dr. Mattias Ulbrich
	Akadem. Oberrat 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 extent)
• Relational Properties of Software for Automated Production Systems

I am also interested in

• Intermediate Verification Languages and Interaction
• Dynamic Logic

Projects

The KeY Project

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

OSLSL
Open-source Teaching Software Laboratory

JML Standard

Committees

• PERR 2019, PC co-chair
• Steering Committee VerifyThis (since 2019)
• Dagstuhl 18-151, co-organiser
• VSTTE 2018, PC member
• PAAR 2018, PC member
• MODELS (Tutorials) 2018, PC member
• VSTTE 2017, PC member
• VerifyThis 2017, Co-organiser
• HFC 2017, PC member
• JML Workshop Bad Herrenalb, 2016, Co-organiser
• Peer reviewing for journals: TOPLAS, at, FMSD, STTT
• lots of subreviewing

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