| 2026 | ENASE | Observable Consistency Checking across Requirements and Models. | Tianhai Liu, Shmuel S. Tyszberowicz, Bernhard Beckert |
| 2026 | FASE | Timed Contract Automata. | Bernhard Beckert, Andreas Bremer, Alexander Weigl |
| 2026 | FASE | Analyses as First-Class Citizens in Model-Driven Development. | Tianhai Liu, Shmuel S. Tyszberowicz, Bernhard Beckert |
| 2025 | FMCAD | Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision. | Samuel Teuber, Debasmita Lohar, Bernhard Beckert |
| 2025 | ICSE | Next Steps in LLM-Supported Java Verification. | Samuel Teuber, Bernhard Beckert |
| 2025 | SMC | Leveraging Industrial Automation Boundaries and Regulation for Scope Reduction in Software Validation. | Yizhi Wang, Birgit Vogel-Heuser, Jan Wilch, Cedric Wagner, Andreas Bremer, Alexander Weigl, Bernhard Beckert |
| 2025 | TACAS | Revisiting Differential Verification: Equivalence Verification with Confidence. | Samuel Teuber, Philipp Kern, Marvin Janzen, Bernhard Beckert |
| 2024 | AAAI | An Information-Flow Perspective on Algorithmic Fairness. | Samuel Teuber, Bernhard Beckert |
| 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 | Towards Combining the Cognitive Abilities of Large Language Models with the Rigor of Deductive Progam Verification. | Bernhard Beckert, Jonas Klamroth, Wolfram Pfeifer, Patrick Rper, Samuel Teuber |
| 2024 | ISoLA | Formal Foundations of Consistency in Model-Driven Development. | Romain Pascual, Bernhard Beckert, Mattias Ulbrich, Michael Kirsten, Wolfram Pfeifer |
| 2024 | MODELS | Towards Formalizing and Relating Different Notions of Consistency in Cyber-Physical Systems Engineering. | Kevin Feichtinger, Karl Kegel, Romain Pascual, Uwe Amann, Bernhard Beckert, Ralf Reussner |
| 2024 | TACAS | Formally Verifying an Efficient Sorter. | Bernhard Beckert, Peter Sanders, Mattias Ulbrich, Julian Wiesler, Sascha Witt |
| 2023 | ICSOC | On Rounding Errors in the Simulation of Quantum Circuits. | Jonas Klamroth, Bernhard Beckert |
| 2023 | MODELS | Consistency in the View-Based Development of Cyber-Physical Systems (Convide). | Ralf Reussner, Ina Schaefer, Bernhard Beckert, Anne Koziolek, Erik Burger |
| 2022 | ESORICS | Why Is Online Voting Still Largely a Black Box? | Michael Kirsten, Melanie Volkamer, Bernhard Beckert |
| 2022 | ICTAC | Generalized Test Tables: A Domain-Specific Specification Language for Automated Production Systems. | Bernhard Beckert, Mattias Ulbrich, Birgit Vogel-Heuser, Alexander Weigl |
| 2022 | ISoLA | Towards a Usable and Sustainable Deductive Verification Tool. | Bernhard Beckert, Richard Bubel, Reiner Hhnle, Mattias Ulbrich |
| 2021 | INDIN | Integration of a formal specification approach into CPPS engineering workflow for machinery validation. | Birgit Vogel-Heuser, Christoph Huber, Suhyun Cha, Bernhard Beckert |
| 2021 | SACMAT | Towards Correct Smart Contracts: A Case Study on Formal Verification of Access Control. | Jonas Schiffl, Matthias Grundmann, Marc Leinweber, Oliver Stengele, Sebastian Friebe, Bernhard Beckert |
| 2020 | ICSE | Towards classes of architectural dependability assurance for machine-learning-based systems. | Max Scheerer, Jonas Klamroth, Ralf Reussner, Bernhard Beckert |
| 2020 | ICSE | Relational Test Tables: A Practical Specification Language for Evolution and Security. | Alexander Weigl, Mattias Ulbrich, Suhyun Cha, Bernhard Beckert, Birgit Vogel-Heuser |
| 2020 | ISoLA | Modular Verification of JML Contracts Using Bounded Model Checking. | Bernhard Beckert, Michael Kirsten, Jonas Klamroth, Mattias Ulbrich |
| 2020 | ISoLA | Specifying Framing Conditions for Smart Contracts. | Bernhard Beckert, Jonas Schiffl |
| 2019 | FM | Smart Contracts: Application Scenarios for Deductive Program Verification. | Bernhard Beckert, Jonas Schiffl, Mattias Ulbrich |
| 2019 | INDIN | 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 |
| 2019 | SAC | Verification-based test case generation for information-flow properties. | Mihai Herda, Shmuel S. Tyszberowicz, Joachim Mssig, Bernhard Beckert |
| 2019 | SEFM | Using Relational Verification for Program Slicing. | Bernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch, Mattias Ulbrich |
| 2018 | ICFEM | Using Theorem Provers to Increase the Precision of Dependence Analysis for Information Flow Control. | Bernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten, Marko Kleine Bning |
| 2018 | ISoLA | Towards a Notion of Coverage for Incomplete Program-Correctness Proofs. | Bernhard Beckert, Mihai Herda, Stefan Kobischke, Mattias Ulbrich |
| 2018 | TAP | Using Dependence Graphs to Assist Verification and Testing of Information-Flow Properties. | Mihai Herda, Shmuel S. Tyszberowicz, Bernhard Beckert |
| 2017 | INDIN | Generation of monitoring functions in production automation using test specifications. | Suhyun Cha, Sebastian Ulewicz, Birgit Vogel-Heuser, Alexander Weigl, Mattias Ulbrich, Bernhard Beckert |
| 2017 | INDIN | 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 |
| 2017 | IFM | SemSlice: Exploiting Relational Verification for Automatic Program Slicing. | Bernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch, Mattias Ulbrich |
| 2017 | IFM | Generalised Test Tables: A Practical Specification Language for Reactive Systems. | Bernhard Beckert, Suhyun Cha, Mattias Ulbrich, Birgit Vogel-Heuser, Alexander Weigl |
| 2017 | SEFM | Modular Verification of Information Flow Security in Component-Based Systems. | Simon Greiner, Martin Mohr, Bernhard Beckert |
| 2017 | SETTA | Computing Exact Loop Bounds for Bounded Program Verification. | Tianhai Liu, Shmuel S. Tyszberowicz, Bernhard Beckert, Mana Taghdiri |
| 2016 | ISoLA | Deductive Verification of Legacy Code. | Bernhard Beckert, Thorsten Bormer, Daniel Grahl |
| 2016 | SETTA | Computing Specification-Sensitive Abstractions for Program Verification. | Tianhai Liu, Shmuel S. Tyszberowicz, Mihai Herda, Bernhard Beckert, Daniel Grahl, Mana Taghdiri |
| 2015 | CADE | Interactive Theorem Proving - Modelling the User in the Proof Process. | Bernhard Beckert, Sarah Grebing |
| 2015 | ECOOP | Regression verification for Java using a secure information flow calculus. | Bernhard Beckert, Vladimir Klebanov, Mattias Ulbrich |
| 2015 | ETFA | Proving equivalence between control software variants for Programmable Logic Controllers. | Sebastian Ulewicz, Birgit Vogel-Heuser, Mattias Ulbrich, Alexander Weigl, Bernhard Beckert |
| 2015 | ICFEM | Regression Verification for Programmable Logic Controller Software. | Bernhard Beckert, Mattias Ulbrich, Birgit Vogel-Heuser, Alexander Weigl |
| 2015 | INDIN | 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, Sinem Getir, Mattias Ulbrich, Vladimir Klebanov, Bernhard Beckert |
| 2014 | SEFM | A Usability Evaluation of Interactive Theorem Provers Using Focus Groups. | Bernhard Beckert, Sarah Grebing, Florian Bhl |
| 2013 | CADE | Dynamic Logic with Trace Semantics. | Bernhard Beckert, Daniel Bruns |
| 2013 | CADE | Analysing Vote Counting Algorithms via Logic - And Its Application to the CADE Election Scheme. | Bernhard Beckert, Rajeev Gor, Carsten Schrmann |
| 2013 | LOPSTR | Information Flow in Object-Oriented Software. | Bernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt, Mattias Ulbrich |
| 2013 | TAP | A Metric for Testing Program Verification Systems. | Bernhard Beckert, Thorsten Bormer, Markus Wagner |
| 2012 | CADE | Evaluating the Usability of Interactive Verification Systems. | Bernhard Beckert, Sarah Grebing |
| 2012 | KI | Formal Semantics of Model Fields in Annotation-Based Specifications. | Bernhard Beckert, Daniel Bruns |
| 2011 | GI | Preface. | Bernhard Beckert |
| 2010 | CADE | Mind the Gap: Formal Verification and the Common Criteria (Discussion Paper). | Bernhard Beckert, Daniel Bruns, Sarah Grebing |
| 2010 | TAP | Generating Regression Unit Tests Using a Combination of Verification and Capture & Replay. | Christoph Gladisch, Shmuel S. Tyszberowicz, Bernhard Beckert, Amiram Yehudai |
| 2009 | KI | Probabilistic Models for the Verification of Human-Computer Interaction. | Bernhard Beckert, Markus Wagner |
| 2009 | SAFECOMP | Formal Verification of a Microkernel Used in Dependable Software Systems. | Christoph Baumann, Bernhard Beckert, Holger Blasum, Thorsten Bormer |
| 2008 | CADE | Title, Preface, Table of Contents. | Bernhard Beckert, Gerwin Klein |
| 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 | SEFM | A Dynamic Logic for Deductive Verification of Concurrent Programs. | Bernhard Beckert, Vladimir Klebanov |
| 2007 | TAP | White-Box Testing by Combining Deduction-Based Specification Extraction and Black-Box Testing. | Bernhard Beckert, Christoph Gladisch |
| 2006 | CADE | Dynamic Logic with Non-rigid Functions. | Bernhard Beckert, Andr Platzer |
| 2006 | ICFEM | A Method for Formalizing, Analyzing, and Verifying Secure User Interfaces. | Bernhard Beckert, Gerd Beuster |
| 2006 | SEFM | Integrating Object-Oriented Design and Deductive Verification of Software. | Bernhard Beckert, Reiner Hhnle, Peter H. Schmitt |
| 2005 | ICFEM | An Improved Rule for While Loops in Deductive Program Verification. | Bernhard Beckert, Steffen Schlager, Peter H. Schmitt |
| 2005 | LPAR | Second-Order Principles in Specification Languages for Object-Oriented Programs. | Bernhard Beckert, Kerry Trentelman |
| 2004 | IFM | Software Verification with Integrated Data Type Refinement for Integer Arithmetic. | Bernhard Beckert, Steffen Schlager |
| 2004 | SEFM | Proof Reuse for Deductive Program Verification. | Bernhard Beckert, Vladimir Klebanov |
| 2003 | FASE | A Program Logic for Handling JAVA CARD's Transaction Mechanism. | Bernhard Beckert, Wojciech Mostowski |
| 2003 | SEFM | Program Verification Using Change Information. | Bernhard Beckert, Peter H. Schmitt |
| 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 |
| 2001 | CADE | A Sequent Calculus for First-Order Dynamic Logic with Trace Modalities. | Bernhard Beckert, Steffen Schlager |
| 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 | CADE | System Description: | Bernhard Beckert, Rajeev Gor |
| 1998 | TABLEAUX | leanK 2.0. | Bernhard Beckert, Rajeev Gor |
| 1998 | TABLEAUX | Fibring Semantic Tableaux. | Bernhard Beckert, Dov M. Gabbay |
| 1998 | TABLEAUX | A Tableau Calculus for Quantifier-Free Set Theoretic Formulae. | Bernhard Beckert, Ulrike Hartmer |
| 1997 | TABLEAUX | Free Variable Tableaux for Propositional Modal Logics. | Bernhard Beckert, Rajeev Gor |
| 1996 | CADE | The Tableau-based Theorem Prover | Bernhard Beckert, Reiner Hhnle, Peter Oel, Martin Sulzmann |
| 1996 | TABLEAUX | Incremental Theory Reasoning Methods for Semantic Tableaux. | Bernhard Beckert, Christian Pape |
| 1995 | CSL | Deduction by Combining Semantic Tableaux and Integer Programming. | Bernhard Beckert, Reiner Hhnle |
| 1995 | CSL | leanEA: A Lean Evolving Algebra Compiler. | Bernhard Beckert, Joachim Posegga |
| 1994 | CADE | A Completion-Based Method for Mixed Universal and Rigid E-Unification. | Bernhard Beckert |
| 1994 | CADE | leanT | Bernhard Beckert, Joachim Posegga |
| 1994 | LPAR | On Anti-Links. | Bernhard Beckert, Reiner Hhnle, Anavai Ramesh, Neil V. Murray |
| 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 |