Integration of Informal and Formal Development of Object-Oriented Safety-Critical Software: A Case Study with the KeY System. - Richard Bubel; Reiner Hähnle (FMICS, 2003)

Ensuring the Correctness of Lightweight Tactics for JavaCard Dynamic Logic. - Richard Bubel; Andreas Roth 002; Philipp Rümmer (LFM@IJCAR, 2004)

The KeY tool. - Wolfgang Ahrendt; Thomas Baar; Bernhard Beckert; Richard Bubel; Martin Giese; Reiner Hähnle; Wolfram Menzel; Wojciech Mostowski; Andreas Roth 002; Steffen Schlager; Peter H. Schmitt (Softw. Syst. Model., 2005)

Integration of informal and formal development of object-oriented safety-critical software. - Richard Bubel; Reiner Hähnle (Int. J. Softw. Tools Technol. Transf., 2005)

Formal verification of recursive predicates. - Richard Bubel (2007)

The Schorr-Waite-Algorithm. - Richard Bubel (The KeY Approach, 2007)

Pattern-Driven Formal Specification. - Richard Bubel; Reiner Hähnle (The KeY Approach, 2007)

Specification Predicates with Explicit Dependency Information. - Richard Bubel; Reiner Hähnle; Peter H. Schmitt (VERIFY, 2008)

Abstract Interpretation of Symbolic Execution with Explicit State Updates. - Richard Bubel; Reiner Hähnle; Benjamin Weiß 001 (FMCO, 2008)

Interleaving Symbolic Execution and Partial Evaluation. - Richard Bubel; Reiner Hähnle; Ran Ji (FMCO, 2009)

Integrated and Tool-Supported Teaching of Testing, Debugging, and Verification. - Wolfgang Ahrendt; Richard Bubel; Reiner Hähnle (TFM, 2009)

Program Specialization via a Software Verification Tool. - Richard Bubel; Reiner Hähnle; Ran Ji (FMCO, 2010)

Specifying Imperative ML-Like Programs Using Dynamic Logic. - Séverine Maingaud; Vincent Balat; Richard Bubel; Reiner Hähnle; Alexandre Miquel (FoVeOOS, 2010)

A visual interactive debugger based on symbolic execution. - Reiner Hähnle; Marcus Baum; Richard Bubel; Marcel Rothe (ASE, 2010)

Verified resource guarantees using COSTA and KeY. - Elvira Albert; Richard Bubel; Samir Genaim; Reiner Hähnle; Germán Puebla; Guillermo Román-Díez (PEPM, 2011)

A Formalisation of Java Strings for Program Specification and Verification. - Richard Bubel; Reiner Hähnle; Ulrich Geilmann (SEFM, 2011)

Verified Resource Guarantees for Heap Manipulating Programs. - Elvira Albert; Richard Bubel; Samir Genaim; Reiner Hähnle; Guillermo Román-Díez (FASE, 2012)

PE-KeY: A Partial Evaluator for Java Programs. - Ran Ji; Richard Bubel (IFM, 2012)

Reuse in Software Verification by Abstract Method Calls. - Reiner Hähnle; Ina Schaefer; Richard Bubel (CADE, 2013)

Program Transformation Based on Symbolic Execution and Deduction. - Ran Ji; Reiner Hähnle; Richard Bubel (SEFM, 2013)

Weak Arithmetic Completeness of Object-Oriented First-Order Assertion Networks. - Stijn de Gouw; Frank S. de Boer; Wolfgang Ahrendt; Richard Bubel (SOFSEM, 2013)

An Interactive Verification Tool Meets an IDE. - Martin Hentschel 002; Stefan Käsdorf; Reiner Hähnle; Richard Bubel (IFM, 2014)

Fully Abstract Operation Contracts. - Richard Bubel; Reiner Hähnle; Maria Pelevina (ISoLA (2), 2014)

Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems. - Crystal Chang Din; Olaf Owe; Richard Bubel (MODELSWARD, 2014)

Symbolic Execution Debugger (SED). - Martin Hentschel 002; Richard Bubel; Reiner Hähnle (RV, 2014)

Analysis of Executable Software Models. - Richard Bubel; Antonio Flores-Montoya; Reiner Hähnle (SFM, 2014)

Visualizing Unbounded Symbolic Execution. - Martin Hentschel 002; Reiner Hähnle; Richard Bubel (TAP@STAF, 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)

KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS. - Crystal Chang Din; Richard Bubel; Reiner Hähnle (CADE, 2015)

OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case. - Stijn de Gouw; Jurriaan Rot; Frank S. de Boer; Richard Bubel; Reiner Hähnle (CAV (1), 2015)

Exploit Generation for Information Flow Leaks in Object-Oriented Programs. - Quoc Huy Do 002; Richard Bubel; Reiner Hähnle (SEC, 2015)

A Dynamic Logic with Traces and Coinduction. - Richard Bubel; Crystal Chang Din; Reiner Hähnle; Keiko Nakata 001 (TABLEAUX, 2015)

Dependency-Based Information Flow Analysis with Declassification in a Program Logic. - Bart van Delft; Richard Bubel (CoRR, 2015)

Testing abstract behavioral specifications. - Peter Y. H. Wong; Richard Bubel; Frank S. de Boer; Miguel Gómez-Zamalloa; Stijn de Gouw; Reiner Hähnle; Karl Meinke; Muddassar Azam Sindhu (Int. J. Softw. Tools Technol. Transf., 2015)

Array Abstraction with Symbolic Pivots. - Reiner Hähnle; Nathan Wasser; Richard Bubel (Theory and Practice of Formal Methods, 2016)

A General Lattice Model for Merging Symbolic Execution Branches. - Dominic Scheurer; Reiner Hähnle; Richard Bubel (ICFEM, 2016)

Can Formal Methods Improve the Efficiency of Code Reviews? - Martin Hentschel 002; Reiner Hähnle; Richard Bubel (IFM, 2016)

An empirical evaluation of two user interfaces of an interactive program verifier. - Martin Hentschel 002; Reiner Hähnle; Richard Bubel (ASE, 2016)

The interactive verification debugger: effective understanding of interactive proof attempts. - Martin Hentschel 002; Reiner Hähnle; Richard Bubel (ASE, 2016)

Proof Repositories for Compositional Verification of Evolving Software Systems - Managing Change When Proving Software Correct. - Richard Bubel; Ferruccio Damiani; Reiner Hähnle; Einar Broch Johnsen; Olaf Owe; Ina Schaefer; Ingrid Chieh Yu (LNCS Trans. Found. Mastering Chang., 2016)

A formal verification framework for static analysis - As well as its instantiation to the resource analyzer COSTA and formal verification tool KeY. - Elvira Albert; Richard Bubel; Samir Genaim; Reiner Hähnle; Germán Puebla; Guillermo Román-Díez (Softw. Syst. Model., 2016)

Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic. - Stijn de Gouw; Frank S. de Boer; Wolfgang Ahrendt; Richard Bubel (Softw. Syst. Model., 2016)

Debugging and Visualization. - Martin Hentschel 002; Reiner Hähnle; Richard Bubel (Deductive Software Verification, 2016)

KeY-Hoare. - Richard Bubel; Reiner Hähnle (Deductive Software Verification, 2016)

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

Program Transformation and Compilation. - Ran Ji; Richard Bubel (Deductive Software Verification, 2016)

Theories. - Peter H. Schmitt; Richard Bubel (Deductive Software Verification, 2016)

Abstract Interpretation. - Nathan Wasser; Reiner Hähnle; Richard Bubel (Deductive Software Verification, 2016)

Inferring Secrets by Guided Experiments. - Quoc Huy Do 002; Richard Bubel; Reiner Hähnle (ICTAC, 2017)

Automatic detection and demonstrator generation for information flow leaks in object-oriented programs. - Quoc Huy Do 002; Richard Bubel; Reiner Hähnle (Comput. Secur., 2017)

Verification of Smart Contract Business Logic - Exploiting a Java Source Code Verifier. - Wolfgang Ahrendt; Richard Bubel; Joshua Ellul; Gordon J. Pace; Raúl Pardo; Vincent Rebiscoul; Gerardo Schneider (FSEN, 2019)

A Program Logic for Dependence Analysis. - Richard Bubel; Reiner Hähnle; Asmae Heydari Tabar (IFM, 2019)

Verifying OpenJDK's Sort Method for Generic Collections. - Stijn de Gouw; Frank S. de Boer; Richard Bubel; Reiner Hähnle; Jurriaan Rot; Dominic Steinhöfel (J. Autom. Reason., 2019)

The Symbolic Execution Debugger (SED): a platform for interactive symbolic execution, debugging, verification and more. - Martin Hentschel 002; Richard Bubel; Reiner Hähnle (Int. J. Softw. Tools Technol. Transf., 2019)

Functional Verification of Smart Contracts via Strong Data Integrity. - Wolfgang Ahrendt; Richard Bubel (ISoLA (3), 2020)

Using Abstract Contracts for Verifying Evolving Features and Their Interactions. - Alexander Knüppel; Stefan Krüger; Thomas Thüm; Richard Bubel; Sebastian Krieter; Eric Bodden; Ina Schaefer (20 Years of KeY, 2020)

Formal Analysis of Smart Contracts: Applying the KeY System. - Jonas Schiffl; Wolfgang Ahrendt; Bernhard Beckert; Richard Bubel (20 Years of KeY, 2020)

Delta-based verification of software product families. - Marco Scaletta; Reiner Hähnle; Dominic Steinhöfel; Richard Bubel (GPCE, 2021)

Finding Semantic Bugs Fast. - Lukas Grätz; Reiner Hähnle; Richard Bubel (FASE, 2022)

Automatic Loop Invariant Generation for Data Dependence Analysis. - Asmae Heydari Tabar; Richard Bubel; Reiner Hähnle (FormaliSE@ICSE, 2022)

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

Towards Trace-based Deductive Verification (Tech Report). - Richard Bubel; Dilian Gurov; Reiner Hähnle; Marco Scaletta (CoRR, 2022)

Examples For FASE NIER Paper "Finding Semantic Bugs Fast". - Lukas Grätz; Reiner Hähnle; Richard Bubel (Zenodo, 2022)

Examples For FASE NIER Paper "Finding Semantic Bugs Fast". - Lukas Grätz; Reiner Hähnle; Richard Bubel (Zenodo, 2022)

Trace-based Deductive Verification. - Richard Bubel; Dilian Gurov; Reiner Hähnle; Marco Scaletta (LPAR, 2023)

SmartML: Enhancing Security and Reliability in Smart Contract Development. - Adele Veschetti; Richard Bubel; Reiner Hähnle (DLT, 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 (FM (2), 2024)

A Formal Modeling Language for Smart Contracts. - Adele Veschetti; Richard Bubel; Reiner Hähnle (SEFM, 2024)

SmartML: Towards a Modeling Language for Smart Contracts. - Adele Veschetti; Richard Bubel; Reiner Hähnle (CoRR, 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)

The Impact of the European Product Liability Directive on Software Engineering. - Doriana Cobârzan; Richard Bubel; Torsten Ullrich (ENASE, 2025)