 |
|
|
| 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 |
|---|---|---|
| Inferring Interval-Valued Floating-Point Preconditions | Jonas Krämer Lionel Blatter Eva Darulova Mattias Ulbrich | Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I |
| Title | Author(s) | Source |
|---|---|---|
| Reconstructing Z3 proofs in KeY: There and back again | Wolfram Pfeifer Jonas Schiffl Mattias Ulbrich | Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs (FTfJP 2021), co-located with ECOOP/ISSTA 2021, Online, 13 July 2021 |
| Scalability and Precision by Combining Expressive Type Systems and Deductive Verification | Florian Lanzinger Alexander Weigl Mattias Ulbrich Werner Dietl | Proceedings of the ACM on programming languages 5(OOPSLA) |
| Deductive Verification of Floating-Point Java Programs in KeY | Rosa Abbasi Jonas Schiffl Eva Darulova Mattias Ulbrich Wolfgang Ahrendt | 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021) held as part of ETAPS 2021: European Joint Conferences on Theory and Practice of Software, Part II |
| Runtime Verification of Generalized Test Tables | Alexander Weigl Mattias Ulbrich Shmuel S. Tyszberowicz Jonas Klamroth | NASA Formal Methods - 13th International Symposium, NFM 2021, Virtual Event, May 24-28, 2021, Proceedings |
| Table-based formal specification approaches for control engineers—empirical studies of usability | Suhyun Cha Birgit Vogel‑Heuser Alexander Weigl Mattias Ulbrich Bernhard Beckert | IET Cyber-Physical Systems: Theory and Applications |
| Title | Author(s) | Source |
|---|---|---|
| Relational Test Tables: A Practical Specification Language for Evolution and Security | Alexander Weigl Mattias Ulbrich Suhyun Cha Bernhard Beckert Birgit Vogel‑Heuser | FormaliSE@ICSE 2020: 8th International Conference on Formal Methods in Software Engineering, Seoul, Republic of Korea, July 13, 2020 |
| Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY | Wolfgang Ahrendt Bernhard Beckert Richard Bubel Reiner Hähnle Mattias Ulbrich | Lecture Notes in Computer Science 12345 (Springer 2020) |
Click here for a full list of my publications.
Supervised Theses
| Title | Year | Type |
|---|---|---|
| Reconstructing Z3 Proofs With KeY | 2021 | M. Sc. |
| Property Types in Java: Combining TypeSystems and Deductive Verification | 2021 | M. Sc. |
| Techniques for Synthesizing Preconditionsfor Floating-Point Functions | 2021 | M. Sc. |
| 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 | ||