 |
|
|
| 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 |
|
Wintersemester 2022/2023
In den Wintersemestern 2022/2023 und 2023/2024 vertrete ich eine vakante Professur an der KIT-Fakultät für Informatik.
Für Fragen zur Vorlesung Grundbegriffe der Informatik können Sie sich an den Übungsleiter Philipp Kern oder mich wenden.
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
Teacher Education
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
Publications
| Title | Author(s) | Source |
|---|---|---|
| Formal Foundations of Consistency in Model-Driven Development | Romain Pascual Bernhard Beckert Mattias Ulbrich Michael Kirsten Wolfram Pfeifer | 12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2024). Specification and Verification |
| Title | Author(s) | Source |
|---|---|---|
| Formally Verifying an Efficient Sorter | Bernhard Beckert Peter Sanders Mattias Ulbrich Sascha Witt Julian Wiesler | Karlsruher Institut für Technologie (KIT) |
| Formally Verifying an Efficient Sorter | Bernhard Beckert Peter Sanders Mattias Ulbrich Sascha Witt Julian Wiesler | International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2024 |
| Title | Author(s) | Source |
|---|---|---|
| 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 |
| Combining rule- and SMT-based reasoning for verifying floating-point Java programs in KeY | Rosa Abbasi Jonas Schiffl Eva Darulova Mattias Ulbrich Wolfgang Ahrendt | Int. J. Softw. Tools Technol. Transf. 25(2) |
| Formal Specification and Verification of JDK's Identity Hash Map Implementation | Martin de Boer Stijn de Gouw Jonas Klamroth Christian Jung Mattias Ulbrich Alexander Weigl | Formal Aspects Comput. 35(3) |
| Neue Einblicke in den Berufswahlprozess von Informatiklehrkräften | Claudia Hildebrandt Barbara Pampel Bernhard Standl Franz J. Hauck Mattias Ulbrich Barbara Paech | Informatikunterricht zwischen Aktualität und Zeitlosigkeit: 20. GI-Fachtagung Informatik und Schule, INFOS 2023, Volume P-336 |
| Title | Author(s) | Source |
|---|---|---|
| Generalized Test Tables: A Domain-Specific Specification Language for Automated Production Systems | Bernhard Beckert Mattias Ulbrich Birgit Vogel‑Heuser Alexander Weigl | Theoretical Aspects of Computing - ICTAC 2022 |
| SpecifyThis - Bridging Gaps Between Program Specification Paradigms | Wolfgang Ahrendt Paula Herber Marieke Huisman Mattias Ulbrich | Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles (ISoLA) 2022 |
| Formal Specification and Verification of JDK’s Identity Hash Map Implementation | Martin de Boer Stijn de Gouw Jonas Klamroth Christian Jung Mattias Ulbrich Alexander Weigl | 17th International Conference on integrated Formal Methods (iFM 2022) |
| Towards a Usable and Sustainable Deductive Verification Tool | Bernhard Beckert Richard Bubel Reiner Hähnle Mattias Ulbrich | Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering (ISoLA) 2022 |
| The Karlsruhe Java Verification Suite | Jonas Klamroth Florian Lanzinger Wolfram Pfeifer Mattias Ulbrich | The Logic of Software. A Tasting Menu of Formal Methods: Essays Dedicated to Reiner Hähnle on the Occasion of His 60th Birthday |
| A Refactoring for Data Minimisation Using Formal Verification | Florian Lanzinger Mattias Ulbrich Alexander Weigl | 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering (ISoLA 2022) |
| Inferring Interval-Valued Floating-Point Preconditions | Jonas Krämer Lionel Blatter Eva Darulova Mattias Ulbrich | 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022), held as part of ETAPS 2022: European Joint Conferences on Theory and Practice of Software, 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 |
|---|---|---|
| Smart Contracts: Application Scenarios for Deductive Program Verification | Bernhard Beckert Jonas Schiffl Mattias Ulbrich | 1st Workshop on Formal Methods for Blockchains (FMBC 2019) hosted by the 3rd Formal Methods World Congress (FM’19) |
| 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 |
| Addressed Challenges | Reiner Jung Lukas Märtin Jan Ole Johanssen Barbara Paech Malte Lochau Thomas Thüm Kurt Schneider Matthias Tichy Mattias Ulbrich | Managed Software Evolution |
| Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning | Emanuele De Angelis Grigory Fedyukovich Nikos Tzevelekos Mattias Ulbrich | abs/1907.03523 2019 |
| Seamless Interactive Program Verification | Sarah Grebing Jonas Klamroth Mattias Ulbrich | 11th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2019) |
| Using Relational Verification for Program Slicing | Bernhard Beckert Thorsten Bormer Stephan Gocht Mihai Herda Daniel Lentzsch Mattias Ulbrich | 17th International Conference on Software Engineering and Formal Methods (SEFM 2019) |
| Using Relational Verification for Program Slicing | Bernhard Beckert Thorsten Bormer Stephan Gocht Mihai Herda Daniel Lentzsch Mattias Ulbrich | Department of Informatics, Karlsruhe Institute of Technology 2019,5 |
| VerifyThis – Verification Competition with a Human Factor | Gidon Ernst Marieke Huisman Wojciech Mostowski Mattias Ulbrich | 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019) |
| Title | Author(s) | Source |
|---|---|---|
| The KeY Platform for Verification and Analysis of Java Programs | Wolfgang Ahrendt Bernhard Beckert Daniel Bruns Richard Bubel Christoph Gladisch Sarah Grebing Reiner Hähnle Martin Hentschel Mihai Herda Vladimir Klebanov Wojciech Mostowski Christoph Scheben Peter H. Schmitt Mattias Ulbrich | 6th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2014) |
| Automating Regression Verification | Dennis Felsing Sarah Grebing Vladimir Klebanov Philipp Rümmer Mattias Ulbrich | 29th IEEE/ACM International Conference on Automated Software Engineering (ASE 2014) |
| JKelloy: A Proof Assistant for Relational Specifications of Java Programs | Aboubakr Achraf El Ghazi Mattias Ulbrich Christoph Gladisch Shmuel Tyszberowicz Mana Taghdiri | 6th NASA Formal Methods Symposium (NFM 2014) |
| Title | Author(s) | Source |
|---|---|---|
| Information Flow in Object-Oriented Software | Bernhard Beckert Daniel Bruns Vladimir Klebanov Christoph Scheben Peter H. Schmitt Mattias Ulbrich | 23rd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2013), Revised Selected Papers |
| Implementation-level verification of algorithms with KeY | Daniel Bruns Wojciech Mostowski Mattias Ulbrich | International Journal on Software Tools for Technology Transfer (STTT) 17(6) |
| Reducing the Complexity of Quantified Formulas via Variable Elimination | Aboubakr Achraf El Ghazi Mattias Ulbrich Mana Taghdiri Mihai Herda | 11th International Workshop on Satisfiability Modulo Theories (SMT 2013) |
| Dynamic Logic for an Intermediate Language: Verification, Interaction and Refinement | Mattias Ulbrich | Karlsruhe Institute of Technology (June 2013) |
| Title | Author(s) | Source |
|---|---|---|
| A Proof Assistant for Alloy Specifications | Mattias Ulbrich Ulrich Geilmann Aboubakr Achraf El Ghazi Mana Taghdiri | 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012) |
| Title | Author(s) | Source |
|---|---|---|
| A Dual-Engine for Early Analysis of Critical Systems | Aboubakr Achraf El Ghazi Ulrich Geilmann Mattias Ulbrich Mana Taghdiri | Workshop on Dependable Software for Critical Infrastructures (DSCI 2011) |
| Dynamic Frames in Java Dynamic Logic | Peter H. Schmitt Mattias Ulbrich Benjamin Weiß | International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), Revised Selected Papers |
| A Dynamic Logic for Unstructured Programs with Embedded Assertions | Mattias Ulbrich | International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), Revised Selected Papers |
| The 1st Verified Software Competition: Experience Report | Vladimir Klebanov Peter Müller Natarajan Shankar Gary T. Leavens Valentin Wüstholz Eyad Alkassar Rob Arthan Derek Bronish Rod Chapman Ernie Cohen Mark Hillebrand Bart Jacobs K. Rustan M. Leino Rosemary Monahan Frank Piessens Nadia Polikarpova Tom Ridge Jan Smans Stephan Tobies Thomas Tuerk Mattias Ulbrich Benjamin Weiß | 17th International Symposium on Formal Methods (FM 2011) |
| Title | Author(s) | Source |
|---|---|---|
| Deductive Verification of a Byzantine Agreement Protocol | Roman Krenický Mattias Ulbrich | Karlsruhe Institute of Technology, Department of Informatics 2010-7 |
| Dynamic Frames in Java Dynamic Logic: Formalisation and Proofs | Peter H. Schmitt Mattias Ulbrich Benjamin Weiß | Department of Computer Science, Karlsruhe Institute of Technology 2010-11 |
| Title | Author(s) | Source |
|---|---|---|
| Software Verification for Java 5 | Mattias Ulbrich | Fakultät für Informatik, Universität Karlsruhe (January 2007) |
| Title | Author(s) | Source |
|---|---|---|
| Bereitstellung und Zuweisung von Ressourcen in der formalen algorithmischen Synthese | Mattias Ulbrich | Fakultät für Informatik, Universität Karlsruhe (January 2005) |
See also my publication lists at: KIT library and DBLP.
Supervised Theses
| Title | Year | Type |
|---|---|---|
| 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 | ||