| 2026 | Coordination | Deductive Verification of Legal Contracts. | Reiner Hhnle, Cosimo Laneve |
| 2026 | FM | Rust yDL: A Program Logic for Rust. | Daniel Drodt, Reiner Hhnle |
| 2025 | FSCD | An Expressive Trace Logic for Recursive Programs. | Dilian Gurov, Reiner Hhnle |
| 2025 | ICST | Equivalent Mutants: Deductive Verification to the Rescue. | Serge Demeyer, Reiner Hhnle |
| 2025 | IFM | Formal Verification of Legal Contracts: A Translation-Based Approach. | Reiner Hhnle, Cosimo Laneve, Adele Veschetti |
| 2025 | TABLEAUX | A Sequent Calculus For Trace Formula Implication. | Niklas Heidler, Reiner Hhnle |
| 2024 | FM | The Java Verification Tool KeY:A Tutorial. | Bernhard Beckert, Richard Bubel, Daniel Drodt, Reiner Hhnle, Florian Lanzinger, Wolfram Pfeifer, Mattias Ulbrich, Alexander Weigl |
| 2024 | ISoLA | Automating Software Re-Engineering Introduction to the ISoLA 2024 Track. | Serge Demeyer, Reiner Hhnle, Heiko Mantel |
| 2024 | ISoLA | Context-Aware Contracts as a Lingua Franca for Behavioral Specification. | Marco Scaletta, Reiner Hhnle |
| 2024 | SEFM | A Formal Modeling Language for Smart Contracts. | Adele Veschetti, Richard Bubel, Reiner Hhnle |
| 2023 | LPAR | Trace-based Deductive Verification. | Richard Bubel, Dilian Gurov, Reiner Hhnle, Marco Scaletta |
| 2023 | SEFM | Herding CATs. | Reiner Hhnle, Marco Scaletta, Eduard Kamburjan |
| 2022 | FASE | Finding Semantic Bugs Fast. | Lukas Grtz, Reiner Hhnle, Richard Bubel |
| 2022 | ISoLA | Towards a Usable and Sustainable Deductive Verification Tool. | Bernhard Beckert, Richard Bubel, Reiner Hhnle, Mattias Ulbrich |
| 2022 | ISoLA | Automating Software Re-engineering: Introduction to the ISoLA 2022 Track. | Serge Demeyer, Reiner Hhnle, Heiko Mantel |
| 2021 | FASE | Certified Abstract Cost Analysis. | Elvira Albert, Reiner Hhnle, Alicia Merayo, Dominic Steinhfel |
| 2021 | GPCE | Delta-based verification of software product families. | Marco Scaletta, Reiner Hhnle, Dominic Steinhfel, Richard Bubel |
| 2021 | SPLC | Variability modules for Java-like languages. | Ferruccio Damiani, Reiner Hhnle, Eduard Kamburjan, Michael Lienhardt, Luca Paolini |
| 2020 | ISoLA | Automating Software Re-engineering - Introduction to the ISoLA 2020 Track. | Serge Demeyer, Reiner Hhnle, Heiko Mantel |
| 2020 | ISoLA | Who Carries the Burden of Modularity? - Introduction to ISoLA 2020 Track on Modularity and (De-)composition in Verification. | Dilian Gurov, Reiner Hhnle, Eduard Kamburjan |
| 2020 | ISoLA | Safer Parallelization. | Reiner Hhnle, Asmae Heydari Tabar, Arya Mazaheri, Mohammad Norouzi, Dominic Steinhfel, Felix Wolf |
| 2019 | FM | Abstract Execution. | Dominic Steinhfel, Reiner Hhnle |
| 2019 | IFM | A Program Logic for Dependence Analysis. | Richard Bubel, Reiner Hhnle, Asmae Heydari Tabar |
| 2019 | SEFM | Asynchronous Cooperative Contracts for Cooperative Scheduling. | Eduard Kamburjan, Crystal Chang Din, Reiner Hhnle, Einar Broch Johnsen |
| 2019 | TAP | The Trace Modality. | Dominic Steinhfel, Reiner Hhnle |
| 2018 | ISoLA | Modular, Correct Compilation with Automatic Soundness Proofs. | Dominic Steinhfel, Reiner Hhnle |
| 2018 | SPLC | Interoperability of software product line variants. | Ferruccio Damiani, Reiner Hhnle, Eduard Kamburjan, Michael Lienhardt |
| 2017 | CADE | 24 Challenges in Deductive Software Verification. | Reiner Hhnle, Marieke Huisman |
| 2017 | FASE | A Unified and Formal Programming Model for Deltas and Traits. | Ferruccio Damiani, Reiner Hhnle, Eduard Kamburjan, Michael Lienhardt |
| 2017 | ICTAC | Inferring Secrets by Guided Experiments. | Quoc Huy Do, Richard Bubel, Reiner Hhnle |
| 2017 | TABLEAUX | Locally Abstract, Globally Concrete Semantics of Concurrent Programming Languages. | Crystal Chang Din, Reiner Hhnle, Einar Broch Johnsen, Ka I Pun, Silvia Lizeth Tapia Tarifa |
| 2017 | TAP | Abstraction Refinement for the Analysis of Software Product Lines. | Ferruccio Damiani, Reiner Hhnle, Michael Lienhardt |
| 2016 | ICFEM | A General Lattice Model for Merging Symbolic Execution Branches. | Dominic Scheurer, Reiner Hhnle, Richard Bubel |
| 2016 | IFM | Can Formal Methods Improve the Efficiency of Code Reviews? | Martin Hentschel, Reiner Hhnle, Richard Bubel |
| 2016 | ISoLA | Correctness-by-Construction and Post-hoc Verification: Friends or Foes? | Maurice H. ter Beek, Reiner Hhnle, Ina Schaefer |
| 2016 | ISoLA | Towards Incremental Validation of Railway Systems. | Reiner Hhnle, Radu Muschevici |
| 2016 | SPLC | A UML profile for delta-oriented programming to support software product line engineering. | Maya R. A. Setyautami, Reiner Hhnle, Radu Muschevici, Ade Azurat |
| 2015 | CADE | KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS. | Crystal Chang Din, Richard Bubel, Reiner Hhnle |
| 2015 | CAV | 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 Hhnle |
| 2015 | ICFEM | History-Based Specification and Verification of Scalable Concurrent and Distributed Systems. | Crystal Chang Din, Silvia Lizeth Tapia Tarifa, Reiner Hhnle, Einar Broch Johnsen |
| 2015 | SEC | Exploit Generation for Information Flow Leaks in Object-Oriented Programs. | Quoc Huy Do, Richard Bubel, Reiner Hhnle |
| 2015 | TABLEAUX | A Dynamic Logic with Traces and Coinduction. | Richard Bubel, Crystal Chang Din, Reiner Hhnle, Keiko Nakata |
| 2014 | APLAS | Resource Analysis of Complex Programs with Cost Equations. | Antonio Flores-Montoya, Reiner Hhnle |
| 2014 | IFM | An Interactive Verification Tool Meets an IDE. | Martin Hentschel, Stefan Ksdorf, Reiner Hhnle, Richard Bubel |
| 2014 | ISoLA | Fully Abstract Operation Contracts. | Richard Bubel, Reiner Hhnle, Maria Pelevina |
| 2014 | ISoLA | Introduction to Track on Engineering Virtualized Services. | Reiner Hhnle, Einar Broch Johnsen |
| 2014 | RV | Symbolic Execution Debugger (SED). | Martin Hentschel, Richard Bubel, Reiner Hhnle |
| 2014 | TAP | Visualizing Unbounded Symbolic Execution. | Martin Hentschel, Reiner Hhnle, Richard Bubel |
| 2013 | CADE | Reuse in Software Verification by Abstract Method Calls. | Reiner Hhnle, Ina Schaefer, Richard Bubel |
| 2013 | SEFM | Program Transformation Based on Symbolic Execution and Deduction. | Ran Ji, Reiner Hhnle, Richard Bubel |
| 2012 | FASE | Verified Resource Guarantees for Heap Manipulating Programs. | Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hhnle, Guillermo Romn-Dez |
| 2012 | ISoLA | Adaptable and Evolving Software for Eternal Systems - (Track Summary). | Reiner Hhnle, Ina Schaefer |
| 2012 | ISoLA | A Liskov Principle for Delta-Oriented Programming. | Reiner Hhnle, Ina Schaefer |
| 2011 | PEPM | Verified resource guarantees using COSTA and KeY. | Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hhnle, Germn Puebla, Guillermo Romn-Dez |
| 2011 | SEFM | A Formalisation of Java Strings for Program Specification and Verification. | Richard Bubel, Reiner Hhnle, Ulrich Geilmann |
| 2010 | ISoLA | HATS: Highly Adaptable and Trustworthy Software Using Formal Methods. | Reiner Hhnle |
| 2010 | ISoLA | Task Forces in the EternalS Coordination Action. | Reiner Hhnle |
| 2010 | SPLC | HATS - A Formal Software Product Line Engineering Methodology. | Dave Clarke, Nikolay Diakov, Reiner Hhnle, Einar Broch Johnsen, Germn Puebla, Balthasar Weitzel, Peter Y. H. Wong |
| 2008 | CADE | Specification Predicates with Explicit Dependency Information. | Richard Bubel, Reiner Hhnle, Peter H. Schmitt |
| 2007 | CADE | The KeY system 1.0 (Deduction Component). | Bernhard Beckert, Martin Giese, Reiner Hhnle, Vladimir Klebanov, Philipp Rmmer, Steffen Schlager, Peter H. Schmitt |
| 2007 | CADE | Symbolic Fault Injection. | Daniel Larsson, Reiner Hhnle |
| 2007 | CADE | KeY-C: A Tool for Verification of C Programs. | Oleg Mrk, Daniel Larsson, Reiner Hhnle |
| 2007 | TAP | Generating Unit Tests from Formal Proofs. | Christian Engel, Reiner Hhnle |
| 2006 | LPAR | Automating Verification of Loops by Parallelization. | Tobias Gedell, Reiner Hhnle |
| 2006 | SEFM | Integrating Object-Oriented Design and Deductive Verification of Software. | Bernhard Beckert, Reiner Hhnle, Peter H. Schmitt |
| 2005 | ISMIS | Normal Forms for Knowledge Compilation. | Reiner Hhnle, Neil V. Murray, Erik Rosenthal |
| 2003 | TABLEAUX | Fair Constraint Merging Tableaux in Lazy Functional Programming Style. | Reiner Hhnle, Niklas Srensson |
| 2002 | FASE | The KeY System: Integrating Object-Oriented Design and Formal Methods. | Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hhnle, Wolfram Menzel, Wojciech Mostowski, Peter H. Schmitt |
| 2002 | FASE | An Authoring Tool for Informal and Formal Requirements Specifications. | Reiner Hhnle, Kristofer Johannisson, Aarne Ranta |
| 2001 | CADE | Ordered Resolution vs. Connection Graph Resolution. | Reiner Hhnle, Neil V. Murray, Erik Rosenthal |
| 2000 | GI | Entwurfsmustergesteuerte Erzeugung von OCL-Constraints. | Thomas Baar, Reiner Hhnle, Theo Sattler, Peter H. Schmitt |
| 2000 | JELIA | The KeY Approach: Integrating Object Oriented Design and Formal Verification. | Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hhnle, Wolfram Menzel, Peter H. Schmitt |
| 1999 | TABLEAUX | Proof Confluent Tableau Calculi. | Reiner Hhnle, Bernhard Beckert |
| 1998 | TABLEAUX | Some Remarks on Completeness, Connection Graph Resolution and Link Deletion. | Reiner Hhnle, Neil V. Murray, Erik Rosenthal |
| 1997 | ISMIS | Completeness for Linear Regular Negation Normal Form Inference Systems. | Reiner Hhnle, Neil V. Murray, Erik Rosenthal |
| 1997 | TABLEAUX | Ordered Tableaux: Extensions and Applications. | Reiner Hhnle, Christian Pape |
| 1996 | CADE | The Tableau-based Theorem Prover | Bernhard Beckert, Reiner Hhnle, Peter Oel, Martin Sulzmann |
| 1995 | CSL | Deduction by Combining Semantic Tableaux and Integer Programming. | Bernhard Beckert, Reiner Hhnle |
| 1994 | CADE | Semantic Tableaux with Ordering Restrictions. | Stefan Klingenbeck, Reiner Hhnle |
| 1994 | LPAR | On Anti-Links. | Bernhard Beckert, Reiner Hhnle, Anavai Ramesh, Neil V. Murray |
| 1993 | ISMIS | Short CNF in Finitely-Valued Logics. | Reiner Hhnle |
| 1993 | LPAR | Verification of Switch-Level Designs with Many-Valued Logic. | Reiner Hhnle, Werner Kernig |
| 1992 | AISC | A New Translation from Deduction into Integer Programming. | Reiner Hhnle |
| 1992 | CADE | The Tableau-Based Theorem Prover | Bernhard Beckert, Stefan Gerberding, Reiner Hhnle, Werner Kernig |
| 1992 | CADE | An Improved Method for Adding Equality to Free Variable Semantic Tableaux. | Bernhard Beckert, Reiner Hhnle |
| 1992 | TABLEAUX | Analytic Tableau and Integer Programming (Extended Abstract). | Reiner Hhnle |
| 1990 | CSL | Towards an Efficient Tableau Proof Procedure for Multiple-Valued Logics. | Reiner Hhnle |
| 1986 | CADE | An Interactive Verification System Based on Dynamic Logic. | Reiner Hhnle, Maritta Heisel, Wolfgang Reif, Werner Stephan |