| 2026 | CAV | Transition Invariants Revisited: Termination Witnesses and Their Validation. | Dirk Beyer, Marek Jankola, Marian Lingsch Rosenfeld |
| 2026 | CAV | SvLibChecker: A Light-Weight Tool for Software Model Checking. | Dirk Beyer, Marian Lingsch Rosenfeld |
| 2026 | FASE | Evaluating Tools for Automatic Software Testing (Report on Test-Comp 2026). | Dirk Beyer |
| 2026 | FASE | Testing in Formal Verification via Witness Generation (Empirical Evaluation). | Dirk Beyer, Thomas Lemberger, Henrik Wachowitz |
| 2026 | TACAS | A Case Study in Firmware Verification: Applying Formal Methods to Intel$^\circledR $ TDX Module. | Dirk Beyer, Po-Chun Chien, Bo-Yuan Huang, Nian-Ze Lee, Thomas Lemberger |
| 2026 | TACAS | Evaluating Software Verifiers for C, Java, and SV-LIB - (Report on SV-COMP 2026). | Dirk Beyer, Jan Strejcek |
| 2025 | FASE | Advances in Automatic Software Testing: Test-Comp 2025. | Dirk Beyer |
| 2025 | FMICS | AutoSV-Annotator: Integrating Deductive and Automatic Software Verification. | Lukas Armborst, Dirk Beyer, Marieke Huisman, Marian Lingsch Rosenfeld |
| 2025 | TACAS | CPAchecker 4.0 as Witness Validator - (Competition Contribution). | Dirk Beyer, Marian Lingsch Rosenfeld |
| 2025 | TACAS | Improvements in Software Verification and Witness Validation: SV-COMP 2025. | Dirk Beyer, Jan Strejcek |
| 2024 | ATVA | CPA-Daemon: Mitigating Tool Restarts for Java-Based Verifiers. | Dirk Beyer, Thomas Lemberger, Henrik Wachowitz |
| 2024 | FM | Software Verification with CPAchecker 3.0: Tutorial and User Guide. | Daniel Baier, Dirk Beyer, Po-Chun Chien, Marie-Christine Jakobs, Marek Jankola, Matthias Kettl, Nian-Ze Lee, Thomas Lemberger, Marian Lingsch Rosenfeld, Henrik Wachowitz, Philipp Wendler |
| 2024 | FM | FM-Weck: Containerized Execution of Formal-Methods Tools. | Dirk Beyer, Henrik Wachowitz |
| 2024 | ICSE | Fault Localization on Verification Witnesses (Poster Paper). | Dirk Beyer, Matthias Kettl, Thomas Lemberger |
| 2024 | MSR | P3: A Dataset of Partial Program Patches. | Dirk Beyer, Lars Grunske, Matthias Kettl, Marian Lingsch Rosenfeld, Moeketsi Raselimo |
| 2024 | TACAS | Btor2-Cert: A Certifying Hardware-Verification Framework Using Software Analyzers. | Zsfia dm, Dirk Beyer, Po-Chun Chien, Nian-Ze Lee, Nils Sirrenberg |
| 2024 | TACAS | CPAchecker 2.3 with Strategy Selection - (Competition Contribution). | Daniel Baier, Dirk Beyer, Po-Chun Chien, Marek Jankola, Matthias Kettl, Nian-Ze Lee, Thomas Lemberger, Marian Lingsch Rosenfeld, Martin Spiessl, Henrik Wachowitz, Philipp Wendler |
| 2024 | TACAS | State of the Art in Software Verification and Witness Validation: SV-COMP 2024. | Dirk Beyer |
| 2023 | FASE | Software Testing: 5th Comparative Evaluation: Test-Comp 2023. | Dirk Beyer |
| 2023 | ICSE | CoVeriTeam Service: Verification as a Service. | Dirk Beyer, Sudeep Kanav, Henrik Wachowitz |
| 2023 | TACAS | Competition on Software Verification and Witness Validation: SV-COMP 2023. | Dirk Beyer |
| 2023 | TACAS | Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Translator. | Dirk Beyer, Po-Chun Chien, Nian-Ze Lee |
| 2023 | VECoS | Safeguarding AI-Based Software Development and Verification using Witnesses (Position Paper). | Dirk Beyer |
| 2022 | FASE | Advances in Automatic Software Testing: Test-Comp 2022. | Dirk Beyer |
| 2022 | FASE | Construction of Verifier Combinations Based on Off-the-Shelf Verifiers. | Dirk Beyer, Sudeep Kanav, Cedric Richter |
| 2022 | ICSE | Decomposing Software Verification into Off-the-Shelf Components: An Application to CEGAR. | Dirk Beyer, Jan Haltermann, Thomas Lemberger, Heike Wehrheim |
| 2022 | SAS | Case Study on Verification-Witness Validators: Where We Are and Where We Go. | Dirk Beyer, Jan Strejcek |
| 2022 | SEFM | A Unifying Approach for Control-Flow-Based Loop Abstraction. | Dirk Beyer, Marian Lingsch Rosenfeld, Martin Spiessl |
| 2022 | SEFM | Cooperation Between Automatic and Interactive Software Verifiers. | Dirk Beyer, Martin Spiessl, Sven Umbricht |
| 2022 | TACAS | Progress on Software Verification: SV-COMP 2022. | Dirk Beyer |
| 2022 | TACAS | CoVeriTeam: On-Demand Composition of Cooperative Verification Systems. | Dirk Beyer, Sudeep Kanav |
| 2022 | TACAS | The Static Analyzer Frama-C in SV-COMP (Competition Contribution). | Dirk Beyer, Martin Spiessl |
| 2021 | ATVA | PJBDD: A BDD Library for Java and Multi-Threading. | Dirk Beyer, Karlheinz Friedberger, Stephan Holzner |
| 2021 | CAV | JavaSMT 3: Interacting with SMT Solvers in Java. | Daniel Baier, Dirk Beyer, Karlheinz Friedberger |
| 2021 | FASE | Status Report on Software Testing: Test-Comp 2021. | Dirk Beyer |
| 2021 | TACAS | Software Verification: 10th Comparative Evaluation (SV-COMP 2021). | Dirk Beyer |
| 2020 | CAV | MetaVal: Witness Validation via Verification. | Dirk Beyer, Martin Spiessl |
| 2020 | FASE | Second Competition on Software Testing: Test-Comp 2020. | Dirk Beyer |
| 2020 | ISoLA | Violation Witnesses and Result Validation for Multi-Threaded Programs - Implementation and Evaluation with CPAchecker. | Dirk Beyer, Karlheinz Friedberger |
| 2020 | ISoLA | An Interface Theory for Program Verification. | Dirk Beyer, Sudeep Kanav |
| 2020 | ISoLA | Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework. | Dirk Beyer, Heike Wehrheim |
| 2020 | ISoLA | Software Verification Tools (Track Introduction). | Markus Schordan, Dirk Beyer, Irena Bojanova |
| 2020 | SEFM | FRed: Conditional Model Checking via Reducers and Folders. | Dirk Beyer, Marie-Christine Jakobs |
| 2020 | SEFM | Difference Verification with Conditions. | Dirk Beyer, Marie-Christine Jakobs, Thomas Lemberger |
| 2020 | TACAS | Software Verification with PDR: An Implementation of the State of the Art. | Dirk Beyer, Matthias Dangl |
| 2020 | TACAS | CPU Energy Meter: A Tool for Energy-Aware Algorithms Engineering. | Dirk Beyer, Philipp Wendler |
| 2020 | TACAS | Advances in Automatic Software Verification: SV-COMP 2020. | Dirk Beyer |
| 2019 | ATVA | Conditional Testing - Off-the-Shelf Combination of Test-Case Generators. | Dirk Beyer, Thomas Lemberger |
| 2019 | FASE | CoVeriTest: Cooperative Verifier-Based Testing. | Dirk Beyer, Marie-Christine Jakobs |
| 2019 | MSR | A data set of program invariants and error paths. | Dirk Beyer |
| 2019 | TACAS | TOOLympics 2019: An Overview of Competitions in Formal Methods. | Ezio Bartocci, Dirk Beyer, Paul E. Black, Grigory Fedyukovich, Hubert Garavel, Arnd Hartmanns, Marieke Huisman, Fabrice Kordon, Julian Nagele, Mihaela Sighireanu, Bernhard Steffen, Martin Suda, Geoff Sutcliffe, Tjark Weber, Akihisa Yamada |
| 2019 | TACAS | Automatic Verification of C and Java Programs: SV-COMP 2019. | Dirk Beyer |
| 2019 | TACAS | International Competition on Software Testing (Test-Comp). | Dirk Beyer |
| 2018 | ICSE | Reducer-based construction of conditional verifiers. | Dirk Beyer, Marie-Christine Jakobs, Thomas Lemberger, Heike Wehrheim |
| 2018 | ISoLA | Strategy Selection for Software Verification Based on Boolean Features - A Simple but Effective Approach. | Dirk Beyer, Matthias Dangl |
| 2018 | ISoLA | In-Place vs. Copy-on-Write CEGAR Refinement for Block Summarization with Caching. | Dirk Beyer, Karlheinz Friedberger |
| 2018 | ISoLA | Evaluating Tools for Software Verification (Track Introduction). | Markus Schordan, Dirk Beyer, Stephen F. Siegel |
| 2018 | TAP | Tests from Witnesses - Execution-Based Validation of Verification Results. | Dirk Beyer, Matthias Dangl, Thomas Lemberger, Michael Tautschnig |
| 2017 | TACAS | Software Verification with Validation of Results - (Report on SV-COMP 2017). | Dirk Beyer |
| 2016 | CAV | Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses. | Dirk Beyer, Matthias Dangl |
| 2016 | ISoLA | Partial Verification and Intermediate Results as a Solution to Combine Automatic and Interactive Verification Techniques. | Dirk Beyer |
| 2016 | ISoLA | Symbolic Execution with CEGAR. | Dirk Beyer, Thomas Lemberger |
| 2016 | ISoLA | Evaluation and Reproducibility of Program Analysis and Verification (Track Introduction). | Markus Schordan, Dirk Beyer, Jonas Lundberg |
| 2016 | TACAS | Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on SV-COMP 2016). | Dirk Beyer |
| 2015 | CAV | Boosting k-Induction with Continuously-Refined Invariants. | Dirk Beyer, Matthias Dangl, Philipp Wendler |
| 2015 | FASE | Facilitating Reuse in Multi-goal Test-Suite Generation for Software Product Lines. | Johannes Brdek, Malte Lochau, Stefan Bauregger, Andreas Holzer, Alexander von Rhein, Sven Apel, Dirk Beyer |
| 2015 | FORTE | Sliced Path Prefixes: An Effective Method to Enable Refinement Selection. | Dirk Beyer, Stefan Lwe, Philipp Wendler |
| 2015 | ICSE | Presence-Condition Simplification in Highly Configurable Systems. | Alexander von Rhein, Alexander Grebhahn, Sven Apel, Norbert Siegmund, Dirk Beyer, Thorsten Berger |
| 2015 | TACAS | Software Verification and Verifiable Witnesses - (Report on SV-COMP 2015). | Dirk Beyer |
| 2014 | CAV | Software Verification in the Google App-Engine Cloud. | Dirk Beyer, Georg Dresler, Philipp Wendler |
| 2014 | ISoLA | Evaluation and Reproducibility of Program Analysis (Track Introduction). | Markus Schordan, Welf Lwe, Dirk Beyer |
| 2014 | TACAS | Status Report on Software Verification - (Competition Summary SV-COMP 2014). | Dirk Beyer |
| 2013 | ESOP | Information Reuse for Multi-goal Reachability Analyses. | Dirk Beyer, Andreas Holzer, Michael Tautschnig, Helmut Veith |
| 2013 | FASE | Explicit-State Software Model Checking Based on CEGAR and Interpolation. | Dirk Beyer, Stefan Lwe |
| 2013 | ICSE | Strategies for product-line verification: case studies and experiments. | Sven Apel, Alexander von Rhein, Philipp Wendler, Armin Grlinger, Dirk Beyer |
| 2013 | TACAS | Second Competition on Software Verification - (Summary of SV-COMP 2013). | Dirk Beyer |
| 2012 | FMCAD | Algorithms for software model checking: Predicate abstraction vs. Impact. | Dirk Beyer, Philipp Wendler |
| 2012 | ISoLA | Linux Driver Verification - (Position Paper). | Dirk Beyer, Alexander K. Petrenko |
| 2012 | ISoLA | The RERS Grey-Box Challenge 2012: Analysis of Event-Condition-Action Systems. | Falk Howar, Malte Isberner, Maik Merten, Bernhard Steffen, Dirk Beyer |
| 2012 | TACAS | Competition on Software Verification - (SV-COMP). | Dirk Beyer |
| 2011 | CAV | CPAchecker: A Tool for Configurable Software Verification. | Dirk Beyer, M. Erkan Keremoglu |
| 2011 | ICSE | Feature cohesion in software product lines: an exploratory study. | Sven Apel, Dirk Beyer |
| 2010 | FASE | Shape Refinement through Explicit Heap Analysis. | Dirk Beyer, Thomas A. Henzinger, Grgory Thoduloz, Damien Zufferey |
| 2010 | FMCAD | Predicate abstraction with adjustable-block encoding. | Dirk Beyer, M. Erkan Keremoglu, Philipp Wendler |
| 2009 | FMCAD | Software model checking via large-block encoding. | Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani |
| 2008 | CAV | CSIsat: Interpolation for LA+EUF. | Dirk Beyer, Damien Zufferey, Rupak Majumdar |
| 2008 | ICSE | CCVisu: automatic visual software decomposition. | Dirk Beyer |
| 2007 | CAV | Algorithms for Interface Synthesis. | Dirk Beyer, Thomas A. Henzinger, Vasu Singh |
| 2007 | CAV | Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis. | Dirk Beyer, Thomas A. Henzinger, Grgory Thoduloz |
| 2007 | HotOS | Don't Settle for Less Than the Best: Use Optimization to Make Decisions. | Kimberly Keeton, Terence Kelly, Arif Merchant, Cipriano A. Santos, Janet L. Wiener, Xiaoyun Zhu, Dirk Beyer |
| 2007 | ICWS | An Application ofWeb-Service Interfaces. | Dirk Beyer, Arindam Chakrabarti, Thomas A. Henzinger, Sanjit A. Seshia |
| 2007 | PLDI | Path invariants. | Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko |
| 2007 | VMCAI | Invariant Synthesis for Combined Theories. | Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko |
| 2006 | CAV | Lazy Shape Analysis. | Dirk Beyer, Thomas A. Henzinger, Grgory Thoduloz |
| 2006 | EuroSys | On the road to recovery: restoring data after disasters. | Kimberly Keeton, Dirk Beyer, Ernesto Brau, Arif Merchant, Cipriano A. Santos, Alex Zhang |
| 2006 | ICSE | Symbolic invariant verification for systems with dynamic structural adaptation. | Basil Becker, Dirk Beyer, Holger Giese, Florian Klein, Daniela Schilling |
| 2006 | ICSE | Relational programming with CrocoPat. | Dirk Beyer |
| 2006 | MSR | Co-change visualization applied to PostgreSQL and ArgoUML: (MSR challenge report). | Dirk Beyer |
| 2006 | NOMS | Self-Adaptive SLA-Driven Capacity Management for Internet Services. | Bruno D. Abrahao, Virglio A. F. Almeida, Jussara M. Almeida, Alex Zhang, Dirk Beyer, Fereydoon Safai |
| 2005 | FASE | Checking Memory Safety with Blast. | Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2005 | IM | Quartermaster - a resource utility system. | Sharad Singhal, Martin F. Arlitt, Dirk Beyer, Sven Graupner, Vijay Machiraju, Jim Pruyne, Jerry Rolia, Akhil Sahai, Cipriano A. Santos, Julie Ward, Xiaoyun Zhu |
| 2005 | WWW | Web service interfaces. | Dirk Beyer, Arindam Chakrabarti, Thomas A. Henzinger |
| 2005 | SIGMETRICS | Deadline scheduling for animation rendering. | Eric Anderson, Dirk Beyer, Kamalika Chaudhuri, Terence Kelly, Norman Salazar, Cipriano A. Santos, Ram Swaminathan, Robert Endre Tarjan, Janet L. Wiener, Yunhong Zhou |
| 2005 | SPAA | Value-maximizing deadline scheduling and its application to animation rendering. | Eric Anderson, Dirk Beyer, Kamalika Chaudhuri, Terence Kelly, Norman Salazar, Cipriano A. Santos, Ram Swaminathan, Robert Endre Tarjan, Janet L. Wiener, Yunhong Zhou |
| 2004 | FAST | Designing for Disasters. | Kimberly Keeton, Cipriano A. Santos, Dirk Beyer, Jeffrey S. Chase, John Wilkes |
| 2004 | ICSE | Generating Tests from Counterexamples. | Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2004 | PEPM | Invited talk: the blast query language for software verification. | Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2004 | PPDP | Invited talk: the blast query language for software verification. | Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2004 | SAS | The Blast Query Language for Software Verification.. | Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2003 | CAV | Rabbit: A Tool for BDD-Based Verification of Real-Time Systems. | Dirk Beyer, Claus Lewerentz, Andreas Noack |
| 2003 | FORTE | Can Decision Diagrams Overcome State Space Explosion in Real-Time Verification? | Dirk Beyer, Andreas Noack |
| 2001 | FM | Improvements in BDD-Based Reachability Analysis of Timed Automata. | Dirk Beyer |