![]() |
|
|
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
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
Title | Author(s) | Source |
---|---|---|
The Many Uses of Dynamic Logic | Wolfgang Ahrendt Bernhard Beckert Richard Bubel Reiner Hähnle Mattias Ulbrich | Go Where the Bugs Are: Essays Dedicated to Wolfgang Reif on the Occasion of His 65th Birthday |
Title | Author(s) | Source |
---|---|---|
The 'Choc-Machine' - an Introduction to Algorithmic Thinking Using Finite State Machines | Annika Vielsack Miriam Klein Thomas Niesenhaus Mattias Ulbrich | Proceedings of the 18th WiPSCE Conference on Primary and Secondary Computing Education Research |
Click here for a full list of my publications.
See also my publication lists at: KIT library and DBLP.
Supervised Theses
Title | Year | Type |
---|---|---|
Bounded Verification of the Static Range Analysis within a JavaScript Engine | 2025 | M. Sc. |
Formal Verification of Java Programs with SQL Database Connectivity | 2024 | B. Sc. |
A Calculus for Set Theory in the Software Verification System KeY | 2024 | B. Sc. |
Predicate Inference for Automatic Java Regression Verification | 2023 | |
Verification of Red-Black Trees in KeY – A Case Study in Deductive Java Verification | 2023 | B. Sc. |
Click here to show all supervised theses |
Teaching
Title | Type |
---|---|
Formale Systeme II: Theorie (SS 22) – bei youtube verfügbar | Lehrbeauftragter |
Teamprojekt Lehramt Informatik (WS 21/221) | (Co-)Betreuung |
Formale Systeme II: Anwendung (SS 21) | Lehrbeauftragter |
Teamprojekt Lehramt Informatik (WS 20/21) | Betreuung |
Formale Systeme II: Theorie (SS 20) | Lehrbeauftragter |
Click here to show all teaching activities |