Armin Biere

ORCID

Publication Activity (10 Years)

Years Active: 1997-2024
Publications (10 Years): 98

Top Venues

Universität Karlsruhe (PHD)

Education History

Universität Karlsruhe

PHD

Publications

Muhammad Osama, Anton Wijs, Armin Biere
Certified SAT solving with GPU accelerated inprocessing. Formal Methods Syst. Des. 62 (1) (2024)
Armin Biere, Katalin Fazekas, Mathias Fleury, Nils Froleyks
Clausal Congruence Closure. SAT (2024)
Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
Disjoint Partial Enumeration without Blocking Clauses. AAAI (2024)
Jean-Marie Lagniez, Pierre Marquis, Armin Biere
Dynamic Blocked Clause Elimination for Projected Model Counting. SAT (2024)
Katalin Fazekas, Florian Pollitt, Mathias Fleury, Armin Biere
Certifying Incremental SAT Solving. LPAR (2024)
Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, Florian Pollitt
CaDiCaL 2.0. CAV (1) (2024)
Nils Froleyks, Emily Yu, Armin Biere, Keijo Heljanko
Certifying Phase Abstraction. CoRR (2024)
Nils Froleyks, Emily Yu, Armin Biere, Keijo Heljanko
Certifying Phase Abstraction. IJCAR (1) (2024)
Cunjing Ge, Armin Biere
Improved Bounds of Integer Solution Counts via Volume and Extending to Mixed-Integer Linear Constraints. CP (2024)
Maximilian Heisinger, Martina Seidl, Armin Biere
ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving. TACAS (1) (2023)
Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
Enumerating Disjoint Partial Models without Blocking Clauses. CoRR (2023)
Nils Froleyks, Emily Yu, Armin Biere
BIG Backbones. FMCAD (2023)
Emily Yu, Nils Froleyks, Armin Biere, Keijo Heljanko
Towards Compositional Hardware Model Checking Certification. FMCAD (2023)
Armin Biere, Nils Froleyks, Wenxi Wang
CadiBack: Extracting Backbones with CaDiCaL. SAT (2023)
Florian Pollitt, Mathias Fleury, Armin Biere
Faster LRAT Checking Than Solving with CaDiCaL. SAT (2023)
Daniela Kaufmann, Armin Biere
Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra. Int. J. Softw. Tools Technol. Transf. 25 (2) (2023)
Armin Biere, Mathias Fleury, Nils Froleyks, Marijn J. H. Heule
The SAT Museum. POS@SAT (2023)
Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere
IPASIR-UP: User Propagators for CDCL. SAT (2023)
Tobias Paxian, Armin Biere
Uncovering and Classifying Bugs in MaxSAT Solvers through Fuzzing and Delta Debugging. POS@SAT (2023)
Emily Yu, Nils Froleyks, Armin Biere, Keijo Heljanko
Stratified Certification for k-Induction. FMCAD (2022)
Jakob Rath, Armin Biere, Laura Kovács
First-Order Subsumption via SAT Solving. FMCAD (2022)
Mathias Fleury, Armin Biere
Mining definitions in Kissat with Kittens. Formal Methods Syst. Des. 60 (3) (2022)
Olaf Beyersdorff, Armin Biere, Vijay Ganesh, Jakob Nordström, Andy Oertel
Theory and Practice of SAT and Combinatorial Solving (Dagstuhl Seminar 22411). Dagstuhl Reports 12 (10) (2022)
Daniela Kaufmann, Armin Biere
Fuzzing and Delta Debugging And-Inverter Graph Verification Tools. TAP@STAF (2022)
Shaowei Cai, Xindi Zhang, Mathias Fleury, Armin Biere
Better Decision Heuristics in CDCL through Local Search and Target Phases. J. Artif. Intell. Res. 74 (2022)
Mathias Fleury, Armin Biere
Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses. CoRR (2022)
Randal E. Bryant, Armin Biere, Marijn J. H. Heule
Clausal Proofs for Pseudo-Boolean Reasoning. TACAS (1) (2022)
Armin Biere, David Parker
Tools and algorithms for the construction and analysis of systems: a special issue for TACAS 2020. Int. J. Softw. Tools Technol. Transf. 24 (5) (2022)
Maximilian Heisinger, Martina Seidl, Armin Biere
QuAPI: Adding Assumptions to Non-Assuming SAT & QBF Solvers. PAAR@IJCAR (2022)
Daniela Kaufmann, Paul Beame, Armin Biere, Jakob Nordström
Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification. DATE (2022)
Emily Yu, Nils Froleyks, Armin Biere, Keijo Heljanko
Stratified Certification for k-Induction. CoRR (2022)
Armin Biere, Md. Solimul Chowdhury, Marijn J. H. Heule, Benjamin Kiesl, Michael W. Whalen
Migrating Solver State. SAT (2022)
Wojciech Nawrocki, Zhenjun Liu, Andreas Fröhlich, Marijn J. H. Heule, Armin Biere
XOR Local Search for Boolean Brent Equations. SAT (2021)
Muhammad Osama, Anton Wijs, Armin Biere
SAT Solving with GPU Accelerated Inprocessing. TACAS (1) (2021)
Mathias Fleury, Armin Biere
Efficient All-UIP Learned Clause Minimization. SAT (2021)
Emily Yu, Armin Biere, Keijo Heljanko
Progress in Certifying Hardware Model Checking Results. CAV (2) (2021)
Sibylle Möhle, Roberto Sebastiani, Armin Biere
On Enumerating Short Projected Models. CoRR (2021)
Lee A. Barnett, Armin Biere
Non-clausal Redundancy Properties. CADE (2021)
Daniela Kaufmann, Armin Biere
AMulet 2.0 for Verifying Multiplier Circuits. TACAS (2) (2021)
Cunjing Ge, Armin Biere
Decomposition Strategies to Count Integer Solutions over Linear Constraints. IJCAI (2021)
Nils Froleyks, Armin Biere
Single Clause Assumption without Activation Literals to Speed-up IC3. FMCAD (2021)
Daniela Kaufmann, Mathias Fleury, Armin Biere
The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus. FMCAD (2020)
Daniela Kaufmann, Armin Biere
Nullstellensatz-Proofs for Multiplier Verification. CASC (2020)
Benjamin Kiesl, Adrián Rebola-Pardo, Marijn J. H. Heule, Armin Biere
Simulating Strong Practical Proof Systems with Extended Resolution. J. Autom. Reason. 64 (7) (2020)
Armin Biere, Cesare Tinelli, Christoph Weidenbach
Preface to the Special Issue on Automated Reasoning Systems. J. Autom. Reason. 64 (3) (2020)
Marijn J. H. Heule, Benjamin Kiesl, Armin Biere
Strong Extension-Free Proof Systems. J. Autom. Reason. 64 (3) (2020)
Maximilian Heisinger, Mathias Fleury, Armin Biere
Distributed Cube and Conquer with Paracooba. SAT (2020)
Daniela Kaufmann, Armin Biere, Manuel Kauers
Incremental column-wise verification of arithmetic circuits using computer algebra. Formal Methods Syst. Des. 56 (1) (2020)
Sibylle Möhle, Roberto Sebastiani, Armin Biere
Four Flavors of Entailment. SAT (2020)
Katalin Fazekas, Markus Sinnl, Armin Biere, Sophie N. Parragh
Duplex Encoding of Staircase At-Most-One Constraints for the Antibandwidth Problem. CPAIOR (2020)
Armin Biere
Tutorial on World-Level Model Checking. FMCAD (2020)
Daniela Kaufmann, Armin Biere, Manuel Kauers
From DRUP to PAC and Back. DATE (2020)
David M. Cerna, Martina Seidl, Wolfgang Schreiner, Wolfgang Windsteiger, Armin Biere
Aiding an Introduction to Formal Reasoning Within a First-Year Logic Course for CS Majors Using a Mobile Self-Study App. ITiCSE (2020)
David M. Cerna, Martina Seidl, Wolfgang Schreiner, Wolfgang Windsteiger, Armin Biere
Computational Logic in the First Semester of Computer Science: An Experience Report. CSEDU (2) (2020)
Lee A. Barnett, David M. Cerna, Armin Biere
Covered Clauses Are Not Propagation Redundant. IJCAR (1) (2020)
Emily Yu, Martina Seidl, Armin Biere
A Framework for Model Checking Against CTLK Using Quantified Boolean Formulas. FTSCS (2019)
Sibylle Möhle, Armin Biere
Combining Conflict-Driven Clause Learning and Chronological Backtracking for Propositional Model Counting. GCAI (2019)
Ankit Shukla, Armin Biere, Luca Pulina, Martina Seidl
A Survey on Applications of Quantified Boolean Formulas. ICTAI (2019)
Marijn J. H. Heule, Benjamin Kiesl, Armin Biere
Encoding Redundancy for Satisfaction-Driven Clause Learning. TACAS (1) (2019)
Zhengqi Yu, Armin Biere, Keijo Heljanko
Certifying Hardware Model Checking Results. ICFEM (2019)
Daniela Ritirc, Armin Biere, Manuel Kauers
SAT, Computer Algebra, Multipliers. Vampire (2019)
Daniela Kaufmann, Armin Biere, Manuel Kauers
Verifying Large Multipliers by Combining SAT and Computer Algebra. FMCAD (2019)
Benjamin Kiesl, Marijn J. H. Heule, Armin Biere
Truth Assignments as Conditional Autarkies. ATVA (2019)
Marijn J. H. Heule, Benjamin Kiesl, Armin Biere
Clausal Proofs of Mutilated Chessboards. NFM (2019)
Sibylle Möhle, Armin Biere
Backing Backtracking. SAT (2019)
Katalin Fazekas, Armin Biere, Christoph Scholl
Incremental Inprocessing in SAT Solving. SAT (2019)
Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere
Local Redundancy in SAT: Generalizations of Blocked Clauses. Log. Methods Comput. Sci. 14 (4) (2018)
Adrián Rebola-Pardo, Armin Biere
Two flavors of DRAT. POS@SAT (2018)
Daniela Ritirc, Armin Biere, Manuel Kauers
A Practical Polynomial Calculus for Arithmetic Circuit Verification. SC-Square@FLOC (2018)
Armin Biere, Andreas Fröhlich
Evaluating CDCL Restart Schemes. POS@SAT (2018)
Sibylle Möhle, Armin Biere
Dualizing Projected Model Counting. ICTAI (2018)
Daniela Ritirc, Armin Biere, Manuel Kauers
Improving and extending the algebraic approach for verifying gate-level multipliers. DATE (2018)
Marijn J. H. Heule, Armin Biere
What a Difference a Variable Makes. TACAS (2) (2018)
Tom van Dijk, Rüdiger Ehlers, Armin Biere
Revisiting Decision Diagrams for SAT. CoRR (2018)
Katalin Fazekas, Fahiem Bacchus, Armin Biere
Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories. IJCAR (2018)
Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere
Btor2 , BtorMC and Boolector 3.0. CAV (1) (2018)
Armin Biere, Marijn Heule
The Effect of Scrambling CNFs. POS@SAT (2018)
Armin Biere, Manuel Kauers, Daniela Ritirc
Challenges in Verifying Arithmetic Circuits Using Computer Algebra. SYNASC (2017)
Daniela Ritirc, Armin Biere, Manuel Kauers
Column-wise verification of multipliers using computer algebra. FMCAD (2017)
Marijn J. H. Heule, Benjamin Kiesl, Armin Biere
Short Proofs Without New Variables. CADE (2017)
Mathias Preiner, Aina Niemetz, Armin Biere
Counterexample-Guided Model Synthesis. TACAS (1) (2017)
Aina Niemetz, Mathias Preiner, Armin Biere
Propagation based local search for bit-precise reasoning. Formal Methods Syst. Des. 51 (3) (2017)
Armin Biere, Steffen Hölldobler, Sibylle Möhle
An Abstract Dual Propositional Model Counter. YSIP (2017)
Marijn J. H. Heule, Benjamin Kiesl, Martina Seidl, Armin Biere
PRuning Through Satisfaction. Haifa Verification Conference (2017)
Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere
Blocked Clauses in First-Order Logic. LPAR (2017)
Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere
Blocked Clauses in First-Order Logic. CoRR (2017)
Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere
Blockedness in Propositional Logic: Are You Satisfied With Your Neighborhood? IJCAI (2017)
Marijn J. H. Heule, Martina Seidl, Armin Biere
Solution Validation and Extraction for QBF Preprocessing. J. Autom. Reason. 58 (1) (2017)
Katalin Fazekas, Marijn J. H. Heule, Martina Seidl, Armin Biere
Skolem Function Continuation for Quantified Boolean Formulas. TAP@STAF (2017)
Aina Niemetz, Mathias Preiner, Armin Biere
Model-Based API Testing for SMT Solvers. SMT (2017)
Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere
Local Redundancy in SAT: Generalizations of Blocked Clauses. CoRR (2017)
Armin Biere, Tom van Dijk, Keijo Heljanko
Hardware model checking competition 2017. FMCAD (2017)
Akihisa Yamada, Armin Biere, Cyrille Artho, Takashi Kitamura, Eun-Hye Choi
Greedy combinatorial test case generation using unsatisfiable cores. ASE (2016)
Gergely Kovásznai, Andreas Fröhlich, Armin Biere
Complexity of Fixed-Size Bit-Vector Logics. Theory Comput. Syst. 59 (2) (2016)
Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere
Super-Blocked Clauses. IJCAR (2016)
Katalin Fazekas, Martina Seidl, Armin Biere
A Duality-Aware Calculus for Quantified Boolean Formulas. SYNASC (2016)
Tomás Balyo, Armin Biere, Markus Iser, Carsten Sinz
SAT Race 2015. Artif. Intell. 241 (2016)
Aina Niemetz, Mathias Preiner, Armin Biere
Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories. CAV (1) (2016)
Akihisa Yamada, Takashi Kitamura, Cyrille Artho, Eun-Hye Choi, Yutaka Oiwa, Armin Biere
Optimization of Combinatorial Testing by Incremental SAT Solving. ICST (2015)
Andreas Fröhlich, Armin Biere, Christoph M. Wintersteiger, Youssef Hamadi
Stochastic Local Search for Satisfiability Modulo Theories. AAAI (2015)

Armin Biere.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Armin Biere