Mattias Ulbrich

Dr. Mattias Ulbrich

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 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

K e Y
The KeY Project
IMPROVE APS
IMPROVE APS
(DFG-SPP1593: Design for Future - Managed Software Evolution)
OSLSL
OSLSL
Open-source Teaching Software Laboratory
IMPROVE APS
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

2024
Title Author(s) Source
Formally Verifying an Efficient SorterBernhard Beckert
Peter Sanders
Mattias Ulbrich
Sascha Witt
Julian Wiesler
Karlsruher Institut für Technologie (KIT)
Formally Verifying an Efficient SorterBernhard Beckert
Peter Sanders
Mattias Ulbrich
Sascha Witt
Julian Wiesler
International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2024
2023
Title Author(s) Source
Scalable and Precise Refinement Types for Imperative LanguagesFlorian 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 KeYRosa 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 ImplementationMartin 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äftenClaudia 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
2022
Title Author(s) Source
Generalized Test Tables: A Domain-Specific Specification Language for Automated Production SystemsBernhard Beckert
Mattias Ulbrich
Birgit Vogel‑Heuser
Alexander Weigl
Theoretical Aspects of Computing - ICTAC 2022
SpecifyThis - Bridging Gaps Between Program Specification ParadigmsWolfgang 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 ImplementationMartin 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 ToolBernhard Beckert
Richard Bubel
Reiner Hähnle
Mattias Ulbrich
Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering (ISoLA) 2022
The Karlsruhe Java Verification SuiteJonas 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 VerificationFlorian Lanzinger
Mattias Ulbrich
Alexander Weigl
Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering (ISoLA) 2022
Inferring Interval-Valued Floating-Point PreconditionsJonas 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
2021
Title Author(s) Source
Reconstructing Z3 proofs in KeY: There and back againWolfram 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 VerificationFlorian Lanzinger
Alexander Weigl
Mattias Ulbrich
Werner Dietl
Proceedings of the ACM on programming languages 5(OOPSLA)
Deductive Verification of Floating-Point Java Programs in KeYRosa 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 TablesAlexander 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 usabilitySuhyun Cha
Birgit Vogel‑Heuser
Alexander Weigl
Mattias Ulbrich
Bernhard Beckert
IET Cyber-Physical Systems: Theory and Applications
2020
Title Author(s) Source
Relational Test Tables: A Practical Specification Language for Evolution and SecurityAlexander 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
Design- and Evaluation-Concept for Teaching and Learning Laboratories in Informatics Teacher EducationBernhard Standl
Anette Bentz
Mattias Ulbrich
Annika Vielsack
Ingo Wagner
Informatics in Schools. Engaging Learners in Computational Thinking - 13th International Conference, ISSEP 2020, Tallinn, Estonia, November 16-18, 2020, Proceedings
Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeYWolfgang Ahrendt
Bernhard Beckert
Richard Bubel
Reiner Hähnle
Mattias Ulbrich
Lecture Notes in Computer Science 12345 (Springer 2020)
The VerifyThis Collaborative Long Term ChallengeMarieke Huisman
Raúl Monti
Mattias Ulbrich
Alexander Weigl
Deductive Software Verification: Future Perspectives: Reflections on the Occasion of 20 Years of KeY, Part IV: Feasibility and Usability
Usability Recommendations for User Guidance in Deductive Program VerificationSarah Grebing
Mattias Ulbrich
Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY, Part IV: Feasibility and Usability
Modular Regression Verification for Reactive SystemsAlexander Weigl
Mattias Ulbrich
Daniel Lentzsch
9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2020), Part II: Engineering Principles
Modular Verification of JML Contracts Using Bounded Model CheckingBernhard Beckert
Michael Kirsten
Jonas Klamroth
Mattias Ulbrich
9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2020), Part I: Verification Principles
VerifyThis Long-term Challenge 2020: Proceedings of the Online-EventMarieke Huisman
Raúl E. Monti
Mattias Ulbrich
Alexander Weigl
Institut für Theoretische Informatik (ITI), KIT 2020
On the Preservation of the Trust by Regression Verification of PLC software for Cyber-Physical Systems of SystemsSuhyun Cha
Mattias Ulbrich
Alexander Weigl
Bernhard Beckert
Kathrin Land
Birgit Vogel‑Heuser
17th IEEE International Conference on Industrial Informatics (INDIN 2019)
2019
Title Author(s) Source
Smart Contracts: Application Scenarios for Deductive Program VerificationBernhard 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 ChangesBernhard Beckert
Jakob Mund
Mattias Ulbrich
Alexander Weigl
Managed Software Evolution
Learning from Evolution for EvolutionStefan 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 ChallengesReiner 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 ReasoningEmanuele De Angelis
Grigory Fedyukovich
Nikos Tzevelekos
Mattias Ulbrich
abs/1907.03523 2019
Seamless Interactive Program VerificationSarah Grebing
Jonas Klamroth
Mattias Ulbrich
11th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2019)
Using Relational Verification for Program SlicingBernhard 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 SlicingBernhard 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 FactorGidon Ernst
Marieke Huisman
Wojciech Mostowski
Mattias Ulbrich
25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019)
2018
Title Author(s) Source
Applicability of Generalized Test Tables: A Case Study Using the Manufacturing System Demonstrator xPPUSuhyun Cha
Alexander Weigl
Mattias Ulbrich
Bernhard Beckert
Birgit Vogel‑Heuser
Automatisierungstechnik 66(10)
Trends in Relational Program VerificationBernhard 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 ProofsBernhard 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 AlgorithmsBernhard 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 TransformationsBernhard 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 ScienceBernhard Beckert
Britta Nestler
Moritz Kiefer
Michael Selzer
Mattias Ulbrich
CoRR abs/1802.02374
Automating Regression Verification of Pointer Programs by Predicate AbstractionVladimir Klebanov
Philipp Rümmer
Mattias Ulbrich
Formal Methods in System Design 52(3)
2017
Title Author(s) Source
VerifyThis 2017: A Program Verification CompetitionMarieke 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 ObjectBernhard Beckert
Sarah Grebing
Mattias Ulbrich
Hardware and Software: Verification and Testing - 13th Haifa Verification Conference (HVC 2017)
Relational Program Reasoning Using Compiler IR – Combining Static Verification and Dynamic AnalysisMoritz Kiefer
Vladimir Klebanov
Mattias Ulbrich
Journal of Automated Reasoning 60(3)
Proving JDK's Dual Pivot Quicksort CorrectBernhard Beckert
Jonas Schiffl
Peter H. Schmitt
Mattias Ulbrich
9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2017)
SemSlice: Exploiting Relational Verification for Automatic Program SlicingBernhard Beckert
Thorsten Bormer
Stephan Gocht
Mihai Herda
Daniel Lentzsch
Mattias Ulbrich
13th International Conference on integrated Formal Methods (iFM 2017)
Generalised Test Tables: A Practical Specification Language for Reactive SystemsBernhard Beckert
Suhyun Cha
Mattias Ulbrich
Birgit Vogel‑Heuser
Alexander Weigl
13th International Conference on integrated Formal Methods (iFM 2017)
Generation of Monitoring Functions in Production Automation Using Test SpecificationsSuhyun Cha
Sebastian Ulewicz
Birgit Vogel‑Heuser
Alexander Weigl
Mattias Ulbrich
Bernhard Beckert
15th IEEE International Conference on Industrial Informatics (INDIN 2017)
Generalized Test Tables: A Powerful and Intuitive Specification Language for Reactive SystemsAlexander Weigl
Franziska Wiebe
Mattias Ulbrich
Sebastian Ulewicz
Suhyun Cha
Michael Kirsten
Bernhard Beckert
Birgit Vogel‑Heuser
15th IEEE International Conference on Industrial Informatics (INDIN 2017)
2016
Title Author(s) Source
Deductive Software Verification - The KeY Book: From Theory to PracticeWolfgang Ahrendt
Bernhard Beckert
Richard Bubel
Reiner Hähnle
Peter H. Schmitt
Mattias Ulbrich
Lecture Notes in Computer Science 10001 (Springer 2016)
From Specification to Proof ObligationsDaniel Grahl
Mattias Ulbrich
Deductive Software Verification - The KeY Book: From Theory to Practice, Part II: Specification and Verification
Modular Specification and VerificationDaniel Grahl
Richard Bubel
Wojciech Mostowski
Peter H. Schmitt
Mattias Ulbrich
Benjamin Weiß
Deductive Software Verification - The KeY Book: From Theory to Practice, Part II: Specification and Verification
Proof Search with TacletsPhilipp Rümmer
Mattias Ulbrich
Deductive Software Verification - The KeY Book: From Theory to Practice, Part I: Foundations
Dynamic Dispatch for Method Contracts through Abstract PredicatesWojciech Mostowski
Mattias Ulbrich
Transactions on Modularity and Composition 1
Relational Program Reasoning Using Compiler IRMoritz Kiefer
Vladimir Klebanov
Mattias Ulbrich
8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2016), Revised Selected Papers
Automated Verification for Functional and Relational Properties of Voting RulesBernhard Beckert
Thorsten Bormer
Michael Kirsten
Till Neuber
Mattias Ulbrich
Sixth International Workshop on Computational Social Choice (COMSOC 2016)
A Verification-Supported Evolution Approach to Assist Software Application Engineers in Industrial Factory AutomationSebastian Ulewicz
Mattias Ulbrich
Alexander Weigl
Michael Kirsten
Franziska Wiebe
Bernhard Beckert
Birgit Vogel‑Heuser
IEEE International Symposium on Assembly and Manufacturing (ISAM 2016)
2015
Title Author(s) Source
A Concept for Multi-Phase Incremental Formal Verification in Robotic Guided SurgeryMattias Ulbrich
Luzie Schreiter
Sarah Grebing
Jörg Raczkowsky
Heinz Wörn
Bernhard Beckert
4th International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2015)
Proving Equivalence between Control Software Variants for Programmable Logic Controllers - Using Regression Verification to Reduce Unneeded Variant DiversitySebastian Ulewicz
Mattias Ulbrich
Alexander Weigl
Bernhard Beckert
Birgit Vogel‑Heuser
20th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2015)
Regression Verification for Programmable Logic Controller SoftwareBernhard Beckert
Mattias Ulbrich
Birgit Vogel‑Heuser
Alexander Weigl
17th International Conference on Formal Engineering Methods (ICFEM 2015)
Regression Verification for Java Using a Secure Information Flow CalculusBernhard Beckert
Vladimir Klebanov
Mattias Ulbrich
17th Workshop on Formal Techniques for Java-like Programs (FTfJP 2015)
Axiomatization of Typed First-Order LogicPeter H. Schmitt
Mattias Ulbrich
20th International Symposium on Formal Methods (FM 2015)
Automating Regression VerificationDennis Felsing
Sarah Grebing
Vladimir Klebanov
Philipp Rümmer
Mattias Ulbrich
Multikonferenz Software Engineering und Management 2015: Fachtagung Software Engineering (SE 2015)
Dynamic Dispatch for Method Contracts through Abstract PredicatesWojciech Mostowski
Mattias Ulbrich
14th International Conference on Modularity (Modularity'15)
2014
Title Author(s) Source
The KeY Platform for Verification and Analysis of Java ProgramsWolfgang 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 VerificationDennis 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 ProgramsAboubakr Achraf El Ghazi
Mattias Ulbrich
Christoph Gladisch
Shmuel Tyszberowicz
Mana Taghdiri
6th NASA Formal Methods Symposium (NFM 2014)
2013
Title Author(s) Source
Information Flow in Object-Oriented SoftwareBernhard 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 KeYDaniel Bruns
Wojciech Mostowski
Mattias Ulbrich
International Journal on Software Tools for Technology Transfer (STTT) 17(6)
Reducing the Complexity of Quantified Formulas via Variable EliminationAboubakr 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 RefinementMattias UlbrichKarlsruhe Institute of Technology (June 2013)
2012
Title Author(s) Source
A Proof Assistant for Alloy SpecificationsMattias 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)
2011
Title Author(s) Source
A Dual-Engine for Early Analysis of Critical SystemsAboubakr Achraf El Ghazi
Ulrich Geilmann
Mattias Ulbrich
Mana Taghdiri
Workshop on Dependable Software for Critical Infrastructures (DSCI 2011)
Dynamic Frames in Java Dynamic LogicPeter 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 AssertionsMattias UlbrichInternational Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), Revised Selected Papers
The 1st Verified Software Competition: Experience ReportVladimir 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)
2010
Title Author(s) Source
Deductive Verification of a Byzantine Agreement ProtocolRoman Krenický
Mattias Ulbrich
Karlsruhe Institute of Technology, Department of Informatics 2010-7
Dynamic Frames in Java Dynamic Logic: Formalisation and ProofsPeter H. Schmitt
Mattias Ulbrich
Benjamin Weiß
Department of Computer Science, Karlsruhe Institute of Technology 2010-11
2007
Title Author(s) Source
Software Verification for Java 5Mattias UlbrichFakultät für Informatik, Universität Karlsruhe (January 2007)
2005
Title Author(s) Source
Bereitstellung und Zuweisung von Ressourcen in der formalen algorithmischen SyntheseMattias UlbrichFakultä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 PdF
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 PdF
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 PdF
Relational Verification of Floating-point Programs 2017 PdF
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 PdF
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 PdF
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
M/B.Sc.=Master/Bachelor, PdF=Praxis der Forschung, StA=Studienarbeit, DA=Diplomarbeit

 

Teaching

Title Type
Lehrbeauftragter
(Co-)Betreuung
Lehrbeauftragter
Betreuung
Lehrbeauftragter
Betreuung
Lehrbeauftragter
Betreuung
VL-Vertretungen
Lehrbeauftragter
Betreuung
VL-Vertretungen
Lehrbeauftragter
VL-Vertretungen
Lehrbeauftragter
Übung zur Vorlesung
Lehrbeauftragter
Proseminar
Übung zur Vorlesung
Übung zur Vorlesung
Übung zur Vorlesung
Übung zur Vorlesung
Praktikum
Seminar
Praktikum
Seminar
Übung zur Vorlesung
Seminar
Übung zur Vorlesung
Click here to show all teaching activities