 |
|
|
| Researcher
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 extend)
- Relational Properties of Software for Automated Production Systems
I am also interested in
- Intermediate Verification Languages and Interaction
- Dynamic Logic
Teacher Eduction
I am a contact person for the degree programme "Lehramt an Gymnasien - Teilstudiengang Informatik" (B.Ed./M.Ed/M.Ed.Erg.).
If you are a student with a question regarding the programme; or if you are interested in enrolling in the programme; feel free to contact me. Alternatively, you can contact the study service center Informatics.
I am coordinating the development for the installation of the teaching lab informatics at KIT.
Projects
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
| Title | Author(s) | Source |
|---|---|---|
| Formal Verification of Evolutionary Changes | Bernhard Beckert Jakob Mund Mattias Ulbrich Alexander Weigl | Managed Software Evolution |
| Learning from Evolution for Evolution | Stefan Kögel Matthias Tichy Abhishek Chakraborty Alexander Fay Birgit Vogel‑Heuser Christopher Haubeck Gabriele Taentzer Timo Kehrer Jan Ladiges Lars Grunske Mattias Ulbrich Safa Bougouffa Sinem Getir Suhyun Cha Udo Kelter Winfried Lamersdorf Kiana Busch Robert Heinrich Sandro Koch | Managed Software Evolution |
Click here for a full list of my publications.
Supervised Theses
| Title | Year | Type |
|---|---|---|
| Modelling and Exploiting Ownership-Annotations Using Dynamic Frames in KeY | 2020 | B. Sc. |
| Ein Rahmenwerk für Experimente zur Evaluation der Verwendung digitaler Medien im Informatikunterricht | 2020 | M. Ed. |
| Specification and Verification of Java Programs with Lambda Expressions | 2019 | B. Sc. |
| Specification and Verification of the Arbitrary Precision Integer Multiplication in Java's BigInteger Class | 2019 | B. Sc. |
| Modular Verification of JML Contracts Using Bounded Model Checking | 2019 | M. Sc. |
| Runtime Monitoring of Event-driven Software Systems Specified Using Interface State Machines: Formal Semantics and Implementation | 2018 | M. Sc. |
| Comparing Deductive Program Verification of Graph Data-Structures | 2018 | B. Sc. |
| Automatic Relational Reasoning for Algebraic Data Types | 2018 | M. Sc. |
| Sampling-based Execution Coverage Estimation for Partially Proved Java Program Specifications | 2018 | M. Sc. |
| Evaluation der Proof-Script-Sprache für KeY | 2018 | B. Sc. |
| A Divide-and-Conquer Strategy with Block and Loop Contracts for Deductive Program Verification | 2018 | B. Sc. |
| Exploiting Runtime Data to Derive Formal Environment Models for the Verification of PLC Software | 2017 | B. Sc. |
| Relational Equivalence Proofs Between Imperative and MapReduce Algorithms | 2017 | |
| Relational Verification of Floating-point Programs | 2017 | |
| Exploiting Runtime Data to Derive Formal Environment Models for the Verification of PLC Software | 2017 | B. Sc. |
| Specifying and Verifying Real-World Java Code with KeY - Case Study java.math.BigInteger | 2017 | B. Sc. |
| Semantic Slicing | 2016 | |
| Dynamic Analysis for Automatic Relational Verification | 2016 | B.Sc. |
| Dual Pivot Quicksort: Specification and Verification using KeY | 2016 | B.Sc. |
| Theory of Refinement of Cyber-Physical Systems into Implementations | 2015 | B.Sc. |
| Regression Verification for Programmable Logic Controller Software | 2015 | M.Sc. |
| Generating Bounded Counterexamples for KeY Proof Obligations | 2014 | M.Sc. |
| Automating Regression Verification | 2014 | |
| Proving Well-Definedness of JML Specifications with KeY | 2013 | StA |
| Design and Implementation of a Verification Framework for Java Bytecode using Unstructured Dynamic Logic | 2012 | DA |
| Introducing the Boogie methodology to USDL | 2011 | StA |
| Verifying Alloy Models Using KeY | 2011 | DA |
| Funktionsabschlüsse in Dynamischer Logik | 2010 | StA |
| Formal Semantics for the Java Modeling Language | 2009 | DA |
| Click here to show all supervised theses | ||