 |
|
|
| 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
Projects
JML Standard
Committees
- 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
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 |
|---|---|---|
| Trends in Relational Program Verification | Bernhard Beckert Mattias Ulbrich | Principled Software Development: Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of his 60th Birthday |
| Towards a Notion of Coverage for Incomplete Program-Correctness Proofs | Bernhard Beckert Mihai Herda Stefan Kobischke Mattias Ulbrich | 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018), Part II: A Broader View on Verification: From Static to Runtime and Back |
| Relational Equivalence Proofs Between Imperative and MapReduce Algorithms | Bernhard Beckert Timo Bingmann Moritz Kiefer Peter Sanders Mattias Ulbrich Alexander Weigl | 10th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2018) |
| Program Equivalence (Dagstuhl Seminar 18151) | Shuvendu K. Lahiri Andrzej Murawski Ofer Strichman Mattias Ulbrich | Dagstuhl Reports 8(4) |
| Proving Equivalence Between Imperative and MapReduce Implementations Using Program Transformations | Bernhard Beckert Timo Bingmann Moritz Kiefer Peter Sanders Mattias Ulbrich Alexander Weigl | rm Proceedings Third Workshop on Models for Formal Analysis of Real Systems rm and Sixth International Workshop on Verification and Program Transformation, rm Thessaloniki, Greece, 20th April 2018 |
| Experience Report: Formal Methods in Material Science | Bernhard Beckert Britta Nestler Moritz Kiefer Michael Selzer Mattias Ulbrich | CoRR abs/1802.02374 |
| Title | Author(s) | Source |
|---|---|---|
| VerifyThis 2017: A Program Verification Competition | Marieke Huisman Rosemary Monahan Wojciech Mostowski Peter Müller Mattias Ulbrich | Karlsruhe Institute of Technology 2017,10 |
| An Interaction Concept for Program Verification Systems with Explicit Proof Object | Bernhard Beckert Sarah Grebing Mattias Ulbrich | Hardware and Software: Verification and Testing - 13th Haifa Verification Conference (HVC 2017) |
Click here for a full list of my publications.
Supervised Theses
| Title | Year | Type |
|---|---|---|
| Runtime Monitoring of Event-driven Software Systems Specified Using Interface State Machines: Formal Semantics and Implementation | 2018 | M. 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 | ||
Teaching
