| 2026 | CAV | Liveness Proofs for Hardware Model Checking. | Nils Froleyks, Emily Yu, Bart Bogaerts, Armin Biere, Keijo Heljanko |
| 2026 | FM | Certifying Constraints in Hardware Model Checking. | Nils Froleyks, Emily Yu, Armin Biere, Keijo Heljanko |
| 2026 | SAT | Factoring Learned Clauses. | Florian Pollitt, Zachary Battleman, Mathias Fleury, Yakir Vizel, Marijn J. H. Heule, Armin Biere, Randal E. Bryant |
| 2026 | SAT | CaDiCaL 3.0 (Tool Paper). | Florian Pollitt, Mathias Fleury, Katalin Fazekas, Nils Froleyks, Andr Schidler, Dominik Schreiber, Armin Biere |
| 2026 | TACAS | Real-time Proof Checking for Distributed Incremental SAT Solving. | Dominik Schreiber, Mathias Fleury, Katalin Fazekas, Armin Biere |
| 2025 | CAV | Introducing Certificates to the Hardware Model Checking Competition. | Nils Froleyks, Emily Yu, Mathias Preiner, Armin Biere, Keijo Heljanko |
| 2025 | FMCAD | Hardware Model Checking Competition 2025. | Armin Biere, Nils Froleyks, Mathias Preiner |
| 2025 | SAT | Streamlining Distributed SAT Solver Design. | Dominik Schreiber, Niccol Rigi-Luperti, Armin Biere |
| 2025 | SAT | Learn to Unlearn. | Bernhard Gstrein, Florian Pollitt, Andr Schidler, Mathias Fleury, Armin Biere |
| 2024 | AAAI | Disjoint Partial Enumeration without Blocking Clauses. | Giuseppe Spallitta, Roberto Sebastiani, Armin Biere |
| 2024 | CAV | CaDiCaL 2.0. | Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, Florian Pollitt |
| 2024 | CP | Improved Bounds of Integer Solution Counts via Volume and Extending to Mixed-Integer Linear Constraints. | Cunjing Ge, Armin Biere |
| 2024 | FMCAD | Clausal Equivalence Sweeping. | Armin Biere, Katalin Fazekas, Mathias Fleury, Nils Froleyks |
| 2024 | FMCAD | Hardware Model Checking Competition 2024. | Armin Biere, Nils Froleyks, Mathias Preiner |
| 2024 | IJCAR | Certifying Phase Abstraction. | Nils Froleyks, Emily Yu, Armin Biere, Keijo Heljanko |
| 2024 | LPAR | Certifying Incremental SAT Solving. | Katalin Fazekas, Florian Pollitt, Mathias Fleury, Armin Biere |
| 2024 | SAT | Clausal Congruence Closure. | Armin Biere, Katalin Fazekas, Mathias Fleury, Nils Froleyks |
| 2024 | SAT | Dynamic Blocked Clause Elimination for Projected Model Counting. | Jean-Marie Lagniez, Pierre Marquis, Armin Biere |
| 2023 | FMCAD | BIG Backbones. | Nils Froleyks, Emily Yu, Armin Biere |
| 2023 | FMCAD | Towards Compositional Hardware Model Checking Certification. | Emily Yu, Nils Froleyks, Armin Biere, Keijo Heljanko |
| 2023 | SAT | The SAT Museum. | Armin Biere, Mathias Fleury, Nils Froleyks, Marijn J. H. Heule |
| 2023 | SAT | CadiBack: Extracting Backbones with CaDiCaL. | Armin Biere, Nils Froleyks, Wenxi Wang |
| 2023 | SAT | IPASIR-UP: User Propagators for CDCL. | Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere |
| 2023 | SAT | Uncovering and Classifying Bugs in MaxSAT Solvers through Fuzzing and Delta Debugging. | Tobias Paxian, Armin Biere |
| 2023 | SAT | Faster LRAT Checking Than Solving with CaDiCaL. | Florian Pollitt, Mathias Fleury, Armin Biere |
| 2023 | TACAS | ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving. | Maximilian Heisinger, Martina Seidl, Armin Biere |
| 2022 | DATE | Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification. | Daniela Kaufmann, Paul Beame, Armin Biere, Jakob Nordstrm |
| 2022 | FMCAD | First-Order Subsumption via SAT Solving. | Jakob Rath, Armin Biere, Laura Kovcs |
| 2022 | FMCAD | Stratified Certification for k-Induction. | Emily Yu, Nils Froleyks, Armin Biere, Keijo Heljanko |
| 2022 | SAT | Migrating Solver State. | Armin Biere, Md. Solimul Chowdhury, Marijn J. H. Heule, Benjamin Kiesl, Michael W. Whalen |
| 2022 | TACAS | Clausal Proofs for Pseudo-Boolean Reasoning. | Randal E. Bryant, Armin Biere, Marijn J. H. Heule |
| 2022 | TAP | Fuzzing and Delta Debugging And-Inverter Graph Verification Tools. | Daniela Kaufmann, Armin Biere |
| 2021 | CADE | Non-clausal Redundancy Properties. | Lee A. Barnett, Armin Biere |
| 2021 | CAV | Progress in Certifying Hardware Model Checking Results. | Emily Yu, Armin Biere, Keijo Heljanko |
| 2021 | FMCAD | Single Clause Assumption without Activation Literals to Speed-up IC3. | Nils Froleyks, Armin Biere |
| 2021 | IJCAI | Decomposition Strategies to Count Integer Solutions over Linear Constraints. | Cunjing Ge, Armin Biere |
| 2021 | SAT | Efficient All-UIP Learned Clause Minimization. | Mathias Fleury, Armin Biere |
| 2021 | SAT | XOR Local Search for Boolean Brent Equations. | Wojciech Nawrocki, Zhenjun Liu, Andreas Frhlich, Marijn J. H. Heule, Armin Biere |
| 2021 | TACAS | AMulet 2.0 for Verifying Multiplier Circuits. | Daniela Kaufmann, Armin Biere |
| 2021 | TACAS | SAT Solving with GPU Accelerated Inprocessing. | Muhammad Osama, Anton Wijs, Armin Biere |
| 2020 | CADE | Covered Clauses Are Not Propagation Redundant. | Lee A. Barnett, David M. Cerna, Armin Biere |
| 2020 | CASC | Nullstellensatz-Proofs for Multiplier Verification. | Daniela Kaufmann, Armin Biere |
| 2020 | CPAIOR | Duplex Encoding of Staircase At-Most-One Constraints for the Antibandwidth Problem. | Katalin Fazekas, Markus Sinnl, Armin Biere, Sophie N. Parragh |
| 2020 | CSEDU | Computational Logic in the First Semester of Computer Science: An Experience Report. | David M. Cerna, Martina Seidl, Wolfgang Schreiner, Wolfgang Windsteiger, Armin Biere |
| 2020 | DATE | From DRUP to PAC and Back. | Daniela Kaufmann, Armin Biere, Manuel Kauers |
| 2020 | FMCAD | Tutorial on World-Level Model Checking. | Armin Biere |
| 2020 | FMCAD | The Proof Checkers Pacheck and Pastque for the Practical Algebraic Calculus. | Daniela Kaufmann, Mathias Fleury, Armin Biere |
| 2020 | ITiCSE | Aiding an Introduction to Formal Reasoning Within a First-Year Logic Course for CS Majors Using a Mobile Self-Study App. | David M. Cerna, Martina Seidl, Wolfgang Schreiner, Wolfgang Windsteiger, Armin Biere |
| 2020 | SAT | Distributed Cube and Conquer with Paracooba. | Maximilian Heisinger, Mathias Fleury, Armin Biere |
| 2020 | SAT | Four Flavors of Entailment. | Sibylle Mhle, Roberto Sebastiani, Armin Biere |
| 2019 | ATVA | Truth Assignments as Conditional Autarkies. | Benjamin Kiesl, Marijn J. H. Heule, Armin Biere |
| 2019 | FMCAD | Verifying Large Multipliers by Combining SAT and Computer Algebra. | Daniela Kaufmann, Armin Biere, Manuel Kauers |
| 2019 | ICFEM | Certifying Hardware Model Checking Results. | Zhengqi Yu, Armin Biere, Keijo Heljanko |
| 2019 | ICTAI | A Survey on Applications of Quantified Boolean Formulas. | Ankit Shukla, Armin Biere, Luca Pulina, Martina Seidl |
| 2019 | SAT | Incremental Inprocessing in SAT Solving. | Katalin Fazekas, Armin Biere, Christoph Scholl |
| 2019 | SAT | Backing Backtracking. | Sibylle Mhle, Armin Biere |
| 2019 | TACAS | Encoding Redundancy for Satisfaction-Driven Clause Learning. | Marijn J. H. Heule, Benjamin Kiesl, Armin Biere |
| 2018 | CADE | Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories. | Katalin Fazekas, Fahiem Bacchus, Armin Biere |
| 2018 | CAV | Btor2 , BtorMC and Boolector 3.0. | Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere |
| 2018 | DATE | Improving and extending the algebraic approach for verifying gate-level multipliers. | Daniela Ritirc, Armin Biere, Manuel Kauers |
| 2018 | ICTAI | Dualizing Projected Model Counting. | Sibylle Mhle, Armin Biere |
| 2018 | SAT | Evaluating CDCL Restart Schemes. | Armin Biere, Andreas Frhlich |
| 2018 | SAT | The Effect of Scrambling CNFs. | Armin Biere, Marijn Heule |
| 2018 | SAT | Two flavors of DRAT. | Adrin Rebola-Pardo, Armin Biere |
| 2018 | TACAS | What a Difference a Variable Makes. | Marijn J. H. Heule, Armin Biere |
| 2017 | CADE | Short Proofs Without New Variables. | Marijn J. H. Heule, Benjamin Kiesl, Armin Biere |
| 2017 | FMCAD | Hardware model checking competition 2017. | Armin Biere, Tom van Dijk, Keijo Heljanko |
| 2017 | FMCAD | Column-wise verification of multipliers using computer algebra. | Daniela Ritirc, Armin Biere, Manuel Kauers |
| 2017 | IJCAI | Blockedness in Propositional Logic: Are You Satisfied With Your Neighborhood? | Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere |
| 2017 | LPAR | Blocked Clauses in First-Order Logic. | Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere |
| 2017 | SYNASC | Challenges in Verifying Arithmetic Circuits Using Computer Algebra. | Armin Biere, Manuel Kauers, Daniela Ritirc |
| 2017 | TACAS | Counterexample-Guided Model Synthesis. | Mathias Preiner, Aina Niemetz, Armin Biere |
| 2017 | TAP | Skolem Function Continuation for Quantified Boolean Formulas. | Katalin Fazekas, Marijn J. H. Heule, Martina Seidl, Armin Biere |
| 2016 | CADE | Super-Blocked Clauses. | Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere |
| 2016 | CAV | Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories. | Aina Niemetz, Mathias Preiner, Armin Biere |
| 2016 | SYNASC | A Duality-Aware Calculus for Quantified Boolean Formulas. | Katalin Fazekas, Martina Seidl, Armin Biere |
| 2015 | AAAI | Stochastic Local Search for Satisfiability Modulo Theories. | Andreas Frhlich, Armin Biere, Christoph M. Wintersteiger, Youssef Hamadi |
| 2015 | FMCAD | Better Lemmas with Lambda Extraction. | Mathias Preiner, Aina Niemetz, Armin Biere |
| 2015 | ICST | Optimization of Combinatorial Testing by Incremental SAT Solving. | Akihisa Yamada, Takashi Kitamura, Cyrille Artho, Eun-Hye Choi, Yutaka Oiwa, Armin Biere |
| 2015 | LPAR | Compositional Propositional Proofs. | Marijn J. H. Heule, Armin Biere |
| 2015 | LPAR | Clausal Proof Compression. | Marijn Heule, Armin Biere |
| 2015 | LPAR | Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination. | Florian Lonsing, Fahiem Bacchus, Armin Biere, Uwe Egly, Martina Seidl |
| 2015 | SAT | Evaluating CDCL Variable Scoring Schemes. | Armin Biere, Andreas Frhlich |
| 2014 | CADE | SAT solving experiments in Vampire. | Armin Biere, Ioan Dragan, Laura Kovcs, Andrei Voronkov |
| 2014 | CADE | A Unified Proof System for QBF Preprocessing. | Marijn Heule, Martina Seidl, Armin Biere |
| 2014 | FMCAD | Challenges in bit-precise reasoning. | Armin Biere |
| 2014 | FMCAD | Efficient extraction of Skolem functions from QRAT proofs. | Marijn Heule, Martina Seidl, Armin Biere |
| 2014 | FMCAD | Turbo-charging Lemmas on demand with don't care reasoning. | Aina Niemetz, Mathias Preiner, Armin Biere |
| 2014 | MFCS | On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic. | Gergely Kovsznai, Helmut Veith, Andreas Frhlich, Armin Biere |
| 2014 | SAT | Improving Implementation of SLS Solvers for SAT and New Heuristics for k-SAT with Long Clauses. | Adrian Balint, Armin Biere, Andreas Frhlich, Uwe Schning |
| 2014 | SAT | Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask). | Toms Balyo, Andreas Frhlich, Marijn Heule, Armin Biere |
| 2014 | SAT | Lingeling Essentials, A Tutorial on Design and Implementation Aspects of the the SAT Solver Lingeling. | Armin Biere |
| 2014 | SAT | Detecting Cardinality Constraints in CNF. | Armin Biere, Daniel Le Berre, Emmanuel Lonca, Norbert Manthey |
| 2014 | SAT | iDQ: Instantiation-Based DQBF Solving. | Andreas Frhlich, Gergely Kovsznai, Armin Biere, Helmut Veith |
| 2013 | ATVA | SmacC: A Retargetable Symbolic Execution Engine. | Armin Biere, Jens Knoop, Laura Kovcs, Jakob Zwirchmayr |
| 2013 | CADE | : A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into. | Gergely Kovsznai, Andreas Frhlich, Armin Biere |
| 2013 | CPAIOR | Revisiting Hyper Binary Resolution. | Marijn Heule, Matti Jrvisalo, Armin Biere |
| 2013 | CSR | More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics with Binary Encoding. | Andreas Frhlich, Gergely Kovsznai, Armin Biere |
| 2013 | DATE | Bridging the gap between dual propagation and CNF-based QBF solving. | Alexandra Goultiaeva, Martina Seidl, Armin Biere |
| 2013 | FMCAD | Lemmas on Demand for Lambdas. | Mathias Preiner, Aina Niemetz, Armin Biere |
| 2013 | LPAR | Blocked Clause Decomposition. | Marijn Heule, Armin Biere |
| 2013 | SAT | Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures. | Martin Aigner, Armin Biere, Christoph M. Kirsch, Aina Niemetz, Mathias Preiner |
| 2013 | SAT | Factoring Out Assumptions to Speed Up MUS Extraction. | Jean-Marie Lagniez, Armin Biere |
| 2013 | TAP | Model-Based Testing for Verification Back-Ends. | Cyrille Artho, Armin Biere, Martina Seidl |
| 2012 | CADE | Practical Aspects of SAT Solving. | Armin Biere |
| 2012 | CADE | Practical Aspects of SAT Solving. | Armin Biere |
| 2012 | CADE | Inprocessing Rules. | Matti Jrvisalo, Marijn Heule, Armin Biere |
| 2012 | CADE | On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width. | Gergely Kovsznai, Andreas Frhlich, Armin Biere |
| 2012 | CADE | qbf2epr: A Tool for Generating EPR Formulas from QBF. | Martina Seidl, Florian Lonsing, Armin Biere |
| 2012 | SAT | Resolution-Based Certificate Extraction for QBF - (Tool Presentation). | Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, Armin Biere |
| 2012 | SAT | Concurrent Cube-and-Conquer - (Poster Presentation). | Peter van der Tak, Marijn Heule, Armin Biere |
| 2012 | SLE | Guided Merging of Sequence Diagrams. | Magdalena Widl, Armin Biere, Petra Brosch, Uwe Egly, Marijn Heule, Gerti Kappel, Martina Seidl, Hans Tompits |
| 2012 | SPLC | A comparison of strategies for tolerating inconsistencies during decision-making. | Alexander Nhrer, Armin Biere, Alexander Egyed |
| 2011 | CADE | Blocked Clause Elimination for QBF. | Armin Biere, Florian Lonsing, Martina Seidl |
| 2011 | SAT | Efficient CNF Simplification Based on Binary Implication Graphs. | Marijn Heule, Matti Jrvisalo, Armin Biere |
| 2011 | SAT | Failed Literal Detection for QBF. | Florian Lonsing, Armin Biere |
| 2010 | LPAR | Clause Elimination Procedures for CNF Formulas. | Marijn Heule, Matti Jrvisalo, Armin Biere |
| 2010 | LPAR | Covered Clause Elimination. | Marijn Heule, Matti Jrvisalo, Armin Biere |
| 2010 | SAT | Automated Testing and Debugging of SAT and QBF Solvers. | Robert Brummayer, Florian Lonsing, Armin Biere |
| 2010 | SAT | Reconstructing Solutions after Blocked Clause Elimination. | Matti Jrvisalo, Armin Biere |
| 2010 | SAT | Integrating Dependency Schemes in Search-Based QBF Solvers. | Florian Lonsing, Armin Biere |
| 2010 | TACAS | Blocked Clause Elimination. | Matti Jrvisalo, Armin Biere, Marijn Heule |
| 2009 | LPNMR | SAT, SMT and Applications. | Armin Biere |
| 2009 | SAT | A Compact Representation for Syntactic Dependencies in QBFs. | Florian Lonsing, Armin Biere |
| 2009 | SAT | Minimizing Learned Clauses. | Niklas Srensson, Armin Biere |
| 2009 | TACAS | Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. | Robert Brummayer, Armin Biere |
| 2008 | FMCAD | Consistency Checking of All Different Constraints over Bit-Vectors within a SAT Solver. | Armin Biere, Robert Brummayer |
| 2008 | SAT | Adaptive Restart Strategies for Conflict Driven SAT Solvers. | Armin Biere |
| 2008 | SAT | Nenofex: Expanding NNF for QBF Solving. | Florian Lonsing, Armin Biere |
| 2007 | CAV | C32SAT: Checking C Expressions. | Robert Brummayer, Armin Biere |
| 2007 | SAT | A First Step Towards a Unified Proof Checker for QBF. | Toni Jussila, Armin Biere, Carsten Sinz, Daniel Krning, Christoph M. Wintersteiger |
| 2006 | CSR | Extended Resolution Proofs for Conjoining BDDs. | Carsten Sinz, Armin Biere |
| 2006 | FM | Enforcer - Efficient Failure Injection. | Cyrille Artho, Armin Biere, Shinichi Honiden |
| 2006 | ICSE | Advanced Unit Testing: How to Scale up a Unit Test Framework. | Cyrille Artho, Armin Biere |
| 2006 | SAT | Extended Resolution Proofs for Symbolic SAT Solving with Quantification. | Toni Jussila, Carsten Sinz, Armin Biere |
| 2005 | SAT | Effective Preprocessing in SAT Through Variable and Clause Elimination. | Niklas En, Armin Biere |
| 2005 | TACAS | Shortest Counterexamples for Symbolic Model Checking of LTL with Past. | Viktor Schuppan, Armin Biere |
| 2005 | VMCAI | Simple Is Better: Efficient Bounded Model Checking for Past LTL. | Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila |
| 2004 | ATVA | Using Block-Local Atomicity to Detect Stale-Value Concurrency Errors. | Cyrille Artho, Klaus Havelund, Armin Biere |
| 2004 | CAV | JNuke: Efficient Dynamic Analysis for Java. | Cyrille Artho, Viktor Schuppan, Armin Biere, Pascal Eugster, Marcel Baur, Boris Zweimller |
| 2004 | FMCAD | Simple Bounded LTL Model Checking. | Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila |
| 2004 | SAT | Resolve and Expand. | Armin Biere |
| 2004 | SAT | Resolve and Expand. | Armin Biere |
| 2002 | ICCAD | SAT and ATPG: Boolean engines for formal hardware verification. | Armin Biere, Wolfgang Kunz |
| 2000 | CAV | Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. | Poul Frederick Williams, Armin Biere, Edmund M. Clarke, Anubhav Gupta |
| 1999 | CAV | Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs. | Armin Biere, Edmund M. Clarke, Richard Raimi, Yunshan Zhu |
| 1999 | DAC | Symbolic Model Checking Using SAT Procedures instead of BDDs. | Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Masahiro Fujita, Yunshan Zhu |
| 1999 | TACAS | Symbolic Model Checking without BDDs. | Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu |
| 1998 | FMCAD | Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification. | Sergey Berezin, Armin Biere, Edmund M. Clarke, Yunshan Zhu |
| 1998 | FMCAD | A Performance Study of BDD-Based Model Checking. | Bwolen Yang, Randal E. Bryant, David R. O'Hallaron, Armin Biere, Olivier Coudert, Geert Janssen, Rajeev K. Ranjan, Fabio Somenzi |
| 1997 | CAV | µcke - Efficient µ-Calculus Model Checking. | Armin Biere |