Dynamic Frames in Java Dynamic Logic. - Peter H. Schmitt; Mattias Ulbrich; Benjamin Weiß 001 (FoVeOOS, 2010)

A Dynamic Logic for Unstructured Programs with Embedded Assertions. - Mattias Ulbrich (FoVeOOS, 2010)

The 1st Verified Software Competition: Experience Report. - Vladimir Klebanov; Peter Müller 001; Natarajan Shankar; Gary T. Leavens; Valentin Wüstholz; Eyad Alkassar; Rob Arthan; Derek Bronish; Rod Chapman; Ernie Cohen; Mark A. Hillebrand; Bart Jacobs 002; et al. (FM, 2011)

The COST IC0701 Verification Competition 2011. - Thorsten Bormer; Marc Brockschmidt; Dino Distefano; Gidon Ernst; Jean-Christophe Filliâtre; Radu Grigore; Marieke Huisman; Vladimir Klebanov; Claude Marché; Rosemary Monahan; Wojciech Mostowski; Nadia Polikarpova; et al. (FoVeOOS, 2011)

A dual-engine for early analysis of critical systems. - Aboubakr Achraf El Ghazi; Mana Taghdiri; Mattias Ulbrich; Ulrich Geilmann (GI-Jahrestagung, 2011)

A Proof Assistant for Alloy Specifications. - Mattias Ulbrich; Ulrich Geilmann; Aboubakr Achraf El Ghazi; Mana Taghdiri (TACAS, 2012)

Information Flow in Object-Oriented Software. - Bernhard Beckert; Daniel Bruns; Vladimir Klebanov; Christoph Scheben; Peter H. Schmitt; Mattias Ulbrich (LOPSTR, 2013)

Dynamic Logic for an Intermediate Language: Verification, Interaction and Refinement. - Mattias Ulbrich (2013)

JKelloy: A Proof Assistant for Relational Specifications of Java Programs. - Aboubakr Achraf El Ghazi; Mattias Ulbrich; Christoph Gladisch; Shmuel S. Tyszberowicz; Mana Taghdiri (NASA Formal Methods, 2014)

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 002; Mihai Herda; Vladimir Klebanov; Wojciech Mostowski; Christoph Scheben; et al. (VSTTE, 2014)

Reducing the Complexity of Quantified Formulas via Variable Elimination. - Aboubakr Achraf El Ghazi; Mattias Ulbrich; Mana Taghdiri; Mihai Herda (CoRR, 2014)

Regression verification for Java using a secure information flow calculus. - Bernhard Beckert; Vladimir Klebanov; Mattias Ulbrich (FTfJP@ECOOP, 2015)

Proving equivalence between control software variants for Programmable Logic Controllers. - Sebastian Ulewicz; Birgit Vogel-Heuser; Mattias Ulbrich; Alexander Weigl; Bernhard Beckert (ETFA, 2015)

Axiomatization of Typed First-Order Logic. - Peter H. Schmitt; Mattias Ulbrich (FM, 2015)

Regression Verification for Programmable Logic Controller Software. - Bernhard Beckert; Mattias Ulbrich; Birgit Vogel-Heuser; Alexander Weigl (ICFEM, 2015)

Selected challenges of software evolution for automated production systems. - Birgit Vogel-Heuser; Stefan Feldmann; Jens Folmer; Jan Ladiges; Alexander Fay; Sascha Lity; Matthias Tichy; Matthias Kowal; Ina Schaefer; Christopher Haubeck; Winfried Lamersdorf; Timo Kehrer; et al. (INDIN, 2015)

Automating Regression Verification. - Dennis Felsing; Sarah Grebing; Vladimir Klebanov; Philipp Rümmer; Mattias Ulbrich (Software Engineering & Management, 2015)

Implementation-level verification of algorithms with KeY. - Daniel Bruns; Wojciech Mostowski; Mattias Ulbrich (Int. J. Softw. Tools Technol. Transf., 2015)

Relational Program Reasoning Using Compiler IR. - Moritz Kiefer; Vladimir Klebanov; Mattias Ulbrich (VSTTE, 2016)

Dynamic Dispatch for Method Contracts Through Abstract Predicates. - Wojciech Mostowski; Mattias Ulbrich (LNCS Trans. Modul. Compos., 2016)

Modular Specification and Verification. - Daniel Grahl; Richard Bubel; Wojciech Mostowski; Peter H. Schmitt; Mattias Ulbrich; Benjamin Weiß 001 (Deductive Software Verification, 2016)

From Specification to Proof Obligations. - Daniel Grahl; Mattias Ulbrich (Deductive Software Verification, 2016)

Proof Search with Taclets. - Philipp Rümmer; Mattias Ulbrich (Deductive Software Verification, 2016)

An Interaction Concept for Program Verification Systems with Explicit Proof Object. - Bernhard Beckert; Sarah Grebing; Mattias Ulbrich (Haifa Verification Conference, 2017)

SemSlice: Exploiting Relational Verification for Automatic Program Slicing. - Bernhard Beckert; Thorsten Bormer; Stephan Gocht; Mihai Herda; Daniel Lentzsch; Mattias Ulbrich (IFM, 2017)

Generalised Test Tables: A Practical Specification Language for Reactive Systems. - Bernhard Beckert; Suhyun Cha; Mattias Ulbrich; Birgit Vogel-Heuser; Alexander Weigl (IFM, 2017)

Generation of monitoring functions in production automation using test specifications. - Suhyun Cha; Sebastian Ulewicz; Birgit Vogel-Heuser; Alexander Weigl; Mattias Ulbrich; Bernhard Beckert (INDIN, 2017)

Generalized test tables: A powerful and intuitive specification language for reactive systems. - Alexander Weigl; Franziska Wiebe; Mattias Ulbrich; Sebastian Ulewicz; Suhyun Cha; Michael Kirsten; Bernhard Beckert; Birgit Vogel-Heuser (INDIN, 2017)

Proving JDK's Dual Pivot Quicksort Correct. - Bernhard Beckert; Jonas Schiffl; Peter H. Schmitt; Mattias Ulbrich (VSTTE, 2017)

Trends in Relational Program Verification. - Bernhard Beckert; Mattias Ulbrich (Principled Software Development, 2018)

Achieving delta description of the control software for an automated production system evolution. - Suhyun Cha; Alexander Weigl; Mattias Ulbrich; Bernhard Beckert; Birgit Vogel-Heuser (CASE, 2018)

Towards a Notion of Coverage for Incomplete Program-Correctness Proofs. - Bernhard Beckert; Mihai Herda; Stefan Kobischke; Mattias Ulbrich (ISoLA (2), 2018)

Relational Equivalence Proofs Between Imperative and MapReduce Algorithms. - Bernhard Beckert; Timo Bingmann; Moritz Kiefer; Peter Sanders 001; Mattias Ulbrich; Alexander Weigl (VSTTE, 2018)

Applicability of generalized test tables: a case study using the manufacturing system demonstrator xPPU. - Suhyun Cha; Alexander Weigl; Mattias Ulbrich; Bernhard Beckert; Birgit Vogel-Heuser (Autom., 2018)

Experience Report: Formal Methods in Material Science. - Bernhard Beckert; Britta Nestler; Moritz Kiefer; Michael Selzer; Mattias Ulbrich (CoRR, 2018)

Proving Equivalence Between Imperative and MapReduce Implementations Using Program Transformations. - Bernhard Beckert; Timo Bingmann; Moritz Kiefer; Peter Sanders 001; Mattias Ulbrich; Alexander Weigl (MARS/VPT@ETAPS, 2018)

Program Equivalence (Dagstuhl Seminar 18151). - Shuvendu K. Lahiri; Andrzej S. Murawski; Ofer Strichman; Mattias Ulbrich (Dagstuhl Reports, 2018)

Automating regression verification of pointer programs by predicate abstraction. - Vladimir Klebanov; Philipp Rümmer; Mattias Ulbrich (Formal Methods Syst. Des., 2018)

Relational Program Reasoning Using Compiler IR - Combining Static Verification and Dynamic Analysis. - Moritz Kiefer; Vladimir Klebanov; Mattias Ulbrich (J. Autom. Reason., 2018)

Formal Verification of Evolutionary Changes. - Bernhard Beckert; Jakob Mund; Mattias Ulbrich; Alexander Weigl (Managed Software Evolution, 2019)

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, 2019)

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; et al. (Managed Software Evolution, 2019)

Smart Contracts: Application Scenarios for Deductive Program Verification. - Bernhard Beckert; Jonas Schiffl; Mattias Ulbrich (FM Workshops (1), 2019)

On the Preservation of the Trust by Regression Verification of PLC software for Cyber-Physical Systems of Systems. - Suhyun Cha; Mattias Ulbrich; Alexander Weigl; Bernhard Beckert; Kathrin Land; Birgit Vogel-Heuser (INDIN, 2019)

Using Relational Verification for Program Slicing. - Bernhard Beckert; Thorsten Bormer; Stephan Gocht; Mihai Herda; Daniel Lentzsch; Mattias Ulbrich (SEFM, 2019)

VerifyThis - Verification Competition with a Human Factor. - Gidon Ernst; Marieke Huisman; Wojciech Mostowski; Mattias Ulbrich (TACAS (3), 2019)

Seamless Interactive Program Verification. - Sarah Grebing; Jonas Klamroth; Mattias Ulbrich (VSTTE, 2019)

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)

Modular Verification of JML Contracts Using Bounded Model Checking. - Bernhard Beckert; Michael Kirsten; Jonas Klamroth; Mattias Ulbrich (ISoLA (1), 2020)

Modular Regression Verification for Reactive Systems. - Alexander Weigl; Mattias Ulbrich; Daniel Lentzsch (ISoLA (2), 2020)

Design- and Evaluation-Concept for Teaching and Learning Laboratories in Informatics Teacher Education. - Bernhard Standl; Anette Bentz; Mattias Ulbrich; Annika Vielsack; Ingo Wagner (ISSEP, 2020)

Usability Recommendations for User Guidance in Deductive Program Verification. - Sarah Grebing; Mattias Ulbrich (20 Years of KeY, 2020)

The VerifyThis Collaborative Long Term Challenge. - Marieke Huisman; Raúl E. Monti; Mattias Ulbrich; Alexander Weigl (20 Years of KeY, 2020)

Reconstructing z3 proofs in KeY: there and back again. - Wolfram Pfeifer; Jonas Schiffl; Mattias Ulbrich (FTfJP@ECOOP, 2021)

Runtime Verification of Generalized Test Tables. - Alexander Weigl; Mattias Ulbrich; Shmuel S. Tyszberowicz; Jonas Klamroth (NFM, 2021)

Deductive Verification of Floating-Point Java Programs in KeY. - Rosa Abbasi; Jonas Schiffl; Eva Darulova; Mattias Ulbrich; Wolfgang Ahrendt (TACAS (2), 2021)

Table-based formal specification approaches for control engineers - empirical studies of usability. - Suhyun Cha; Birgit Vogel-Heuser; Alexander Weigl; Mattias Ulbrich; Bernhard Beckert (IET Cyper-Phys. Syst.: Theory & Appl., 2021)

Scalability and precision by combining expressive type systems and deductive verification. - Florian Lanzinger; Alexander Weigl; Mattias Ulbrich; Werner Dietl (Proc. ACM Program. Lang., 2021)

The Karlsruhe Java Verification Suite. - Jonas Klamroth; Florian Lanzinger; Wolfram Pfeifer; Mattias Ulbrich (The Logic of Software. A Tasting Menu of Formal Methods, 2022)

Generalized Test Tables: A Domain-Specific Specification Language for Automated Production Systems. - Bernhard Beckert; Mattias Ulbrich; Birgit Vogel-Heuser; Alexander Weigl (ICTAC, 2022)

SpecifyThis - Bridging Gaps Between Program Specification Paradigms. - Wolfgang Ahrendt; Paula Herber; Marieke Huisman; Mattias Ulbrich (ISoLA (1), 2022)

Towards a Usable and Sustainable Deductive Verification Tool. - Bernhard Beckert; Richard Bubel; Reiner Hähnle; Mattias Ulbrich (ISoLA (2), 2022)

A Refactoring for Data Minimisation Using Formal Verification. - Florian Lanzinger; Mattias Ulbrich; Alexander Weigl (ISoLA (2), 2022)

Inferring Interval-Valued Floating-Point Preconditions. - Jonas Krämer; Lionel Blatter; Eva Darulova; Mattias Ulbrich (TACAS (1), 2022)

Scalable and Precise Refinement Types for Imperative Languages. - Florian Lanzinger; Joshua Bachmeier; Mattias Ulbrich; Werner Dietl (iFM, 2023)

Neue Einblicke in den Berufswahlprozess von Informatiklehrkräften. - Claudia Hildebrandt; Barbara Pampel; Bernhard Standl; Franz J. Hauck; Mattias Ulbrich; Barbara Paech (INFOS, 2023)

The VerifyThis Collaborative Long-Term Challenge Series. - Wolfgang Ahrendt; Gidon Ernst; Paula Herber; Marieke Huisman; Raúl E. Monti; Mattias Ulbrich; Alexander Weigl (TOOLympics@ETAPS, 2023)

The 'Choc-Machine' - an Introduction to Algorithmic Thinking using Finite State Machines. - Annika Vielsack; Miriam Klein; Thomas Niesenhaus; Mattias Ulbrich (WiPSCE, 2023)

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., 2023)

Formal Specification and Verification of JDK's Identity Hash Map Implementation. - Martin de Boer; Stijn de Gouw; Jonas Klamroth; Christian Jung 003; Mattias Ulbrich; Alexander Weigl (Formal Aspects Comput., 2023)

Formally Verifying an Efficient Sorter - Verification and Benchmarking Artifact. - Bernhard Beckert; Peter Sanders 001; Mattias Ulbrich; Julian Wiesler; Sascha Witt (Zenodo, 2023)

The Java Verification Tool KeY:A Tutorial. - Bernhard Beckert; Richard Bubel; Daniel Drodt; Reiner Hähnle; Florian Lanzinger; Wolfram Pfeifer; Mattias Ulbrich; Alexander Weigl (FM (2), 2024)

Contract Automata: A Specification Language for Mode-Based Systems. - Alexander Weigl; Joshua Bachmeier; Bernhard Beckert; Mattias Ulbrich (FormaliSE@ICSE, 2024)

SpecifyThis Bridging Gaps Between Program Specification Paradigms: Track Introduction. - Gidon Ernst; Paula Herber; Marieke Huisman; Mattias Ulbrich (ISoLA (3), 2024)

Contract-LIB: A Proposal for a Common Interchange Format for Software System Specification. - Gidon Ernst; Wolfram Pfeifer; Mattias Ulbrich (ISoLA (3), 2024)

Formal Foundations of Consistency in Model-Driven Development. - Romain Pascual; Bernhard Beckert; Mattias Ulbrich; Michael Kirsten; Wolfram Pfeifer (ISoLA (3), 2024)

Formally Verifying an Efficient Sorter. - Bernhard Beckert; Peter Sanders 001; Mattias Ulbrich; Julian Wiesler; Sascha Witt (TACAS (1), 2024)

The Java Verification Tool KeY: A Tutorial. - Bernhard Beckert; Richard Bubel; Daniel Drodt; Reiner Hähnle; Florian Lanzinger; Wolfram Pfeifer; Mattias Ulbrich; Alexander Weigl (Zenodo, 2024)

KeY CLI, Release 2.13. - Wolfgang Ahrendt; Bernhard Beckert; Richard Bubel; Reiner Hähnle; Mattias Ulbrich; Alexander Weigl (Zenodo, 2024)

The Many Uses of Dynamic Logic. - Wolfgang Ahrendt; Bernhard Beckert; Richard Bubel; Reiner Hähnle; Mattias Ulbrich (Go Where the Bugs Are, 2025)

Heterogeneous Dynamic Logic: Provability Modulo Program Theories. - Samuel Teuber; Mattias Ulbrich; André Platzer; Bernhard Beckert (CoRR, 2025)