 |
|
|
| 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
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 |
|---|---|---|
| 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 |
| Scalable and Precise Refinement Types for Imperative Languages | Florian Lanzinger Joshua Bachmeier Mattias Ulbrich Werner Dietl | iFM 2023 - 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13-15, 2023, Proceedings |
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. |
| LiquidRust: Refinement Types for Imperative Languages with Ownership | 2022 | M. Sc. |
| Parallel Deductive Verification of Dafny through Pure Portfolios | 2022 | M. Sc. |
| Cooperative Specification Extraction for KeY | 2022 | |
| Generating Mutation Tests Using an Equivalence Prover | 2022 | |
| Formal Specification and Verification of a Java Implementation of Super Scalar Sample Sort | 2022 | M. Sc. |
| Property Types for Mutable Data Structures in Java | 2022 | M. Sc. |
| A Formal Notion of Leakage Regression for Timed Automata | 2022 | B. Sc. |
| Specification and Verification of Hash Table Data Structures with KeY | 2021 | B. Sc. |
| Reconstructing Z3 Proofs With KeY | 2021 | M. Sc. |
| Property Types in Java: Combining TypeSystems and Deductive Verification | 2021 | M. Sc. |
| Techniques for Synthesizing Preconditions for Floating-Point Functions | 2021 | M. Sc. |
| Using Machine Learning to Improve Strategy Selection in KeY | 2020 | |
| 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 | ||