Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDArmin Biere
Person information
- affiliation: Universität Freiburg, Germany
- affiliation (former): Johannes Kepler University of Linz, Austria
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2023
[j32]Daniela Kaufmann
, Armin Biere:
Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra. Int. J. Softw. Tools Technol. Transf. 25(2): 133-144 (2023)- [c168]Armin Biere, Nils Froleyks, Wenxi Wang:
CadiBack: Extracting Backbones with CaDiCaL. SAT 2023: 3:1-3:12 - [c167]Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere:
IPASIR-UP: User Propagators for CDCL. SAT 2023: 8:1-8:13 - [c166]Florian Pollitt, Mathias Fleury, Armin Biere:
Faster LRAT Checking Than Solving with CaDiCaL. SAT 2023: 21:1-21:12 - [c165]Maximilian Heisinger, Martina Seidl, Armin Biere:
ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving. TACAS (1) 2023: 426-447 - [i12]Giuseppe Spallitta, Roberto Sebastiani, Armin Biere:
Enumerating Disjoint Partial Models without Blocking Clauses. CoRR abs/2306.00461 (2023) - 2022
- [j31]Shaowei Cai, Xindi Zhang, Mathias Fleury, Armin Biere:
Better Decision Heuristics in CDCL through Local Search and Target Phases. J. Artif. Intell. Res. 74: 1515-1563 (2022) - [j30]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): 663-665 (2022) - [c164]Daniela Kaufmann, Paul Beame, Armin Biere, Jakob Nordström:
Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification. DATE 2022: 1431-1436 - [c163]Emily Yu, Nils Froleyks, Armin Biere, Keijo Heljanko:
Stratified Certification for k-Induction. FMCAD 2022: 59-64 - [c162]Jakob Rath, Armin Biere, Laura Kovács:
First-Order Subsumption via SAT Solving. FMCAD 2022: 160-169 - [c161]Maximilian Heisinger, Martina Seidl, Armin Biere:
QuAPI: Adding Assumptions to Non-Assuming SAT & QBF Solvers. PAAR@IJCAR 2022 - [c160]Armin Biere, Md. Solimul Chowdhury, Marijn J. H. Heule, Benjamin Kiesl, Michael W. Whalen:
Migrating Solver State. SAT 2022: 27:1-27:24 - [c159]Randal E. Bryant, Armin Biere, Marijn J. H. Heule:
Clausal Proofs for Pseudo-Boolean Reasoning. TACAS (1) 2022: 443-461 - [c158]Daniela Kaufmann, Armin Biere:
Fuzzing and Delta Debugging And-Inverter Graph Verification Tools. TAP@STAF 2022: 69-88 - [i11]Mathias Fleury, Armin Biere:
Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses. CoRR abs/2207.13577 (2022) - [i10]Emily Yu, Nils Froleyks, Armin Biere, Keijo Heljanko:
Stratified Certification for k-Induction. CoRR abs/2208.01443 (2022) - [i9]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): 84-105 (2022) - 2021
- [c157]Lee A. Barnett, Armin Biere:
Non-clausal Redundancy Properties. CADE 2021: 252-272 - [c156]Emily Yu, Armin Biere, Keijo Heljanko:
Progress in Certifying Hardware Model Checking Results. CAV (2) 2021: 363-386 - [c155]Nils Froleyks, Armin Biere:
Single Clause Assumption without Activation Literals to Speed-up IC3. FMCAD 2021: 72-76 - [c154]Cunjing Ge, Armin Biere:
Decomposition Strategies to Count Integer Solutions over Linear Constraints. IJCAI 2021: 1389-1395 - [c153]Mathias Fleury, Armin Biere:
Efficient All-UIP Learned Clause Minimization. SAT 2021: 171-187 - [c152]Wojciech Nawrocki, Zhenjun Liu, Andreas Fröhlich, Marijn J. H. Heule, Armin Biere:
XOR Local Search for Boolean Brent Equations. SAT 2021: 417-435 - [c151]Muhammad Osama, Anton Wijs, Armin Biere:
SAT Solving with GPU Accelerated Inprocessing. TACAS (1) 2021: 133-151 - [c150]Daniela Kaufmann, Armin Biere:
AMulet 2.0 for Verifying Multiplier Circuits. TACAS (2) 2021: 357-364 - [p5]Armin Biere, Matti Järvisalo, Benjamin Kiesl:
Preprocessing in SAT Solving. Handbook of Satisfiability 2021: 391-435 - [p4]Armin Biere:
Bounded Model Checking. Handbook of Satisfiability 2021: 739-764 - [e13]Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh:
Handbook of Satisfiability - Second Edition. Frontiers in Artificial Intelligence and Applications 336, IOS Press 2021, ISBN 978-1-64368-160-3 [contents] - [i8]Sibylle Möhle, Roberto Sebastiani, Armin Biere:
On Enumerating Short Projected Models. CoRR abs/2110.12924 (2021) - 2020
- [j29]Daniela Kaufmann, Armin Biere, Manuel Kauers:
Incremental column-wise verification of arithmetic circuits using computer algebra. Formal Methods Syst. Des. 56(1): 22-54 (2020) - [j28]Armin Biere, Cesare Tinelli, Christoph Weidenbach:
Preface to the Special Issue on Automated Reasoning Systems. J. Autom. Reason. 64(3): 361-362 (2020) - [j27]Marijn J. H. Heule, Benjamin Kiesl, Armin Biere:
Strong Extension-Free Proof Systems. J. Autom. Reason. 64(3): 533-554 (2020) - [j26]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): 1247-1267 (2020) - [c149]Lee A. Barnett, David M. Cerna, Armin Biere:
Covered Clauses Are Not Propagation Redundant. IJCAR (1) 2020: 32-47 - [c148]Daniela Kaufmann, Armin Biere:
Nullstellensatz-Proofs for Multiplier Verification. CASC 2020: 368-389 - [c147]Katalin Fazekas, Markus Sinnl, Armin Biere, Sophie N. Parragh:
Duplex Encoding of Staircase At-Most-One Constraints for the Antibandwidth Problem. CPAIOR 2020: 186-204 - [c146]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: 374-381 - [c145]Daniela Kaufmann, Armin Biere, Manuel Kauers:
From DRUP to PAC and Back. DATE 2020: 654-657 - [c144]Armin Biere:
Tutorial on World-Level Model Checking. FMCAD 2020: 1 - [c143]Daniela Kaufmann, Mathias Fleury, Armin Biere:
The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus. FMCAD 2020: 264-269 - [c142]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: 61-67 - [c141]Sibylle Möhle, Roberto Sebastiani, Armin Biere:
Four Flavors of Entailment. SAT 2020: 62-71 - [c140]Maximilian Heisinger, Mathias Fleury, Armin Biere:
Distributed Cube and Conquer with Paracooba. SAT 2020: 114-122 - [e12]Armin Biere, David Parker:
Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I. Lecture Notes in Computer Science 12078, Springer 2020, ISBN 978-3-030-45189-9 [contents] - [e11]Armin Biere, David Parker:
Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part II. Lecture Notes in Computer Science 12079, Springer 2020, ISBN 978-3-030-45236-0 [contents]
2010 – 2019
- 2019
- [c139]Benjamin Kiesl, Marijn J. H. Heule, Armin Biere:
Truth Assignments as Conditional Autarkies. ATVA 2019: 48-64 - [c138]Daniela Kaufmann, Armin Biere, Manuel Kauers:
Verifying Large Multipliers by Combining SAT and Computer Algebra. FMCAD 2019: 28-36 - [c137]Emily Yu, Martina Seidl, Armin Biere:
A Framework for Model Checking Against CTLK Using Quantified Boolean Formulas. FTSCS 2019: 127-132 - [c136]Sibylle Möhle, Armin Biere:
Combining Conflict-Driven Clause Learning and Chronological Backtracking for Propositional Model Counting. GCAI 2019: 113-126 - [c135]Zhengqi Yu, Armin Biere, Keijo Heljanko:
Certifying Hardware Model Checking Results. ICFEM 2019: 498-502 - [c134]Ankit Shukla, Armin Biere, Luca Pulina, Martina Seidl:
A Survey on Applications of Quantified Boolean Formulas. ICTAI 2019: 78-84 - [c133]Marijn J. H. Heule, Benjamin Kiesl, Armin Biere:
Clausal Proofs of Mutilated Chessboards. NFM 2019: 204-210 - [c132]Katalin Fazekas, Armin Biere, Christoph Scholl:
Incremental Inprocessing in SAT Solving. SAT 2019: 136-154 - [c131]Sibylle Möhle, Armin Biere:
Backing Backtracking. SAT 2019: 250-266 - [c130]Marijn J. H. Heule, Benjamin Kiesl, Armin Biere:
Encoding Redundancy for Satisfaction-Driven Clause Learning. TACAS (1) 2019: 41-58 - [c129]Daniela Ritirc, Armin Biere, Manuel Kauers:
SAT, Computer Algebra, Multipliers. Vampire 2019: 1-18 - 2018
- [j25]Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere:
Local Redundancy in SAT: Generalizations of Blocked Clauses. Log. Methods Comput. Sci. 14(4) (2018) - [c128]Katalin Fazekas, Fahiem Bacchus, Armin Biere:
Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories. IJCAR 2018: 134-151 - [c127]Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere:
Btor2 , BtorMC and Boolector 3.0. CAV (1) 2018: 587-595 - [c126]Daniela Ritirc, Armin Biere, Manuel Kauers:
Improving and extending the algebraic approach for verifying gate-level multipliers. DATE 2018: 1556-1561 - [c125]Sibylle Möhle, Armin Biere:
Dualizing Projected Model Counting. ICTAI 2018: 702-709 - [c124]Armin Biere, Andreas Fröhlich:
Evaluating CDCL Restart Schemes. POS@SAT 2018: 1-17 - [c123]Adrián Rebola-Pardo, Armin Biere:
Two flavors of DRAT. POS@SAT 2018: 94-110 - [c122]Armin Biere, Marijn Heule:
The Effect of Scrambling CNFs. POS@SAT 2018: 111-126 - [c121]Daniela Ritirc, Armin Biere, Manuel Kauers:
A Practical Polynomial Calculus for Arithmetic Circuit Verification. SC-Square@FLOC 2018: 61 - [c120]Marijn J. H. Heule, Armin Biere:
What a Difference a Variable Makes. TACAS (2) 2018: 75-92 - [p3]Marijn J. H. Heule, Oliver Kullmann, Armin Biere:
Cube-and-Conquer for Satisfiability. Handbook of Parallel Constraint Reasoning 2018: 31-59 - [p2]Armin Biere, Daniel Kröning:
SAT-Based Model Checking. Handbook of Model Checking 2018: 277-303 - [i7]Tom van Dijk, Rüdiger Ehlers, Armin Biere:
Revisiting Decision Diagrams for SAT. CoRR abs/1805.03496 (2018) - 2017
- [j24]Aina Niemetz, Mathias Preiner, Armin Biere:
Propagation based local search for bit-precise reasoning. Formal Methods Syst. Des. 51(3): 608-636 (2017) - [j23]Marijn J. H. Heule, Martina Seidl, Armin Biere:
Solution Validation and Extraction for QBF Preprocessing. J. Autom. Reason. 58(1): 97-125 (2017) - [c119]Marijn J. H. Heule, Benjamin Kiesl, Armin Biere:
Short Proofs Without New Variables. CADE 2017: 130-147 - [c118]Armin Biere, Tom van Dijk, Keijo Heljanko:
Hardware model checking competition 2017. FMCAD 2017: 9 - [c117]Daniela Ritirc, Armin Biere, Manuel Kauers:
Column-wise verification of multipliers using computer algebra. FMCAD 2017: 23-30 - [c116]Marijn J. H. Heule, Benjamin Kiesl, Martina Seidl, Armin Biere:
PRuning Through Satisfaction. Haifa Verification Conference 2017: 179-194 - [c115]Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere:
Blockedness in Propositional Logic: Are You Satisfied With Your Neighborhood? IJCAI 2017: 4884-4888 - [c114]Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere:
Blocked Clauses in First-Order Logic. LPAR 2017: 31-48 - [c113]Aina Niemetz, Mathias Preiner, Armin Biere:
Model-Based API Testing for SMT Solvers. SMT 2017: 3-14 - [c112]Armin Biere, Manuel Kauers, Daniela Ritirc:
Challenges in Verifying Arithmetic Circuits Using Computer Algebra. SYNASC 2017: 9-15 - [c111]Mathias Preiner, Aina Niemetz, Armin Biere:
Counterexample-Guided Model Synthesis. TACAS (1) 2017: 264-280 - [c110]Katalin Fazekas, Marijn J. H. Heule, Martina Seidl, Armin Biere:
Skolem Function Continuation for Quantified Boolean Formulas. TAP@STAF 2017: 129-138 - [c109]Armin Biere, Steffen Hölldobler, Sibylle Möhle:
An Abstract Dual Propositional Model Counter. YSIP 2017: 17-26 - [i6]Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere:
Blocked Clauses in First-Order Logic. CoRR abs/1702.00847 (2017) - [i5]Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere:
Local Redundancy in SAT: Generalizations of Blocked Clauses. CoRR abs/1702.05527 (2017) - 2016
- [j22]Tomás Balyo, Armin Biere, Markus Iser, Carsten Sinz:
SAT Race 2015. Artif. Intell. 241: 45-65 (2016) - [j21]Gergely Kovásznai, Andreas Fröhlich, Armin Biere:
Complexity of Fixed-Size Bit-Vector Logics. Theory Comput. Syst. 59(2): 323-376 (2016) - [c108]Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere:
Super-Blocked Clauses. IJCAR 2016: 45-61 - [c107]Aina Niemetz, Mathias Preiner, Armin Biere:
Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories. CAV (1) 2016: 199-217 - [c106]Akihisa Yamada, Armin Biere, Cyrille Artho, Takashi Kitamura, Eun-Hye Choi:
Greedy combinatorial test case generation using unsatisfiable cores. ASE 2016: 614-624 - [c105]Katalin Fazekas, Martina Seidl, Armin Biere:
A Duality-Aware Calculus for Quantified Boolean Formulas. SYNASC 2016: 181-186 - 2015
- [j20]Marijn Heule, Matti Järvisalo, Florian Lonsing, Martina Seidl, Armin Biere:
Clause Elimination for SAT and QSAT. J. Artif. Intell. Res. 53: 127-168 (2015) - [c104]Andreas Fröhlich, Armin Biere, Christoph M. Wintersteiger, Youssef Hamadi:
Stochastic Local Search for Satisfiability Modulo Theories. AAAI 2015: 1136-1143 - [c103]Mathias Preiner, Aina Niemetz, Armin Biere:
Better Lemmas with Lambda Extraction. FMCAD 2015: 128-135 - [c102]Akihisa Yamada, Takashi Kitamura, Cyrille Artho, Eun-Hye Choi, Yutaka Oiwa, Armin Biere:
Optimization of Combinatorial Testing by Incremental SAT Solving. ICST 2015: 1-10 - [c101]Marijn Heule, Armin Biere:
Clausal Proof Compression. IWIL@LPAR 2015: 21-26 - [c100]Florian Lonsing, Fahiem Bacchus, Armin Biere, Uwe Egly, Martina Seidl:
Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination. LPAR 2015: 418-433 - [c99]Marijn J. H. Heule, Armin Biere:
Compositional Propositional Proofs. LPAR 2015: 444-459 - [c98]Marijn Heule, Martina Seidl, Armin Biere:
Blocked Literals Are Universal. NFM 2015: 436-442 - [c97]Armin Biere, Andreas Fröhlich:
Evaluating CDCL Variable Scoring Schemes. SAT 2015: 405-422 - [i4]Armin Biere, Vijay Ganesh, Martin Grohe, Jakob Nordström, Ryan Williams:
Theory and Practice of SAT Solving (Dagstuhl Seminar 15171). Dagstuhl Reports 5(4): 98-122 (2015) - 2014
- [j19]Aina Niemetz, Mathias Preiner, Armin Biere:
Boolector 2.0. J. Satisf. Boolean Model. Comput. 9(1): 53-58 (2014) - [j18]Gianpiero Cabodi, Carmelo Loiacono, Marco Palena, Paolo Pasini, Denis Patti, Stefano Quer, Danilo Vendraminetto, Armin Biere, Keijo Heljanko:
Hardware Model Checking Competition 2014: An Analysis and Comparison of Solvers and Benchmarks. J. Satisf. Boolean Model. Comput. 9(1): 135-172 (2014) - [j17]Gilles Audemard, Armin Biere, Jean-Marie Lagniez, Laurent Simon:
Améliorer SAT dans le cadre incrémental. Rev. d'Intelligence Artif. 28(5): 593-614 (2014) - [c96]Armin Biere, Ioan Dragan, Laura Kovács, Andrei Voronkov:
SAT solving experiments in Vampire. Vampire Workshop 2014: 29-32 - [c95]Marijn Heule, Martina Seidl, Armin Biere:
A Unified Proof System for QBF Preprocessing. IJCAR 2014: 91-106 - [c94]Armin Biere:
Challenges in bit-precise reasoning. FMCAD 2014: 3 - [c93]Marijn Heule, Martina Seidl, Armin Biere:
Efficient extraction of Skolem functions from QRAT proofs. FMCAD 2014: 107-114 - [c92]Aina Niemetz, Mathias Preiner, Armin Biere:
Turbo-charging Lemmas on demand with don't care reasoning. FMCAD 2014: 179-186 - [c91]Gergely Kovásznai, Helmut Veith, Andreas Fröhlich, Armin Biere:
On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic. MFCS (2) 2014: 481-492 - [c90]Armin Biere, Ioan Dragan, Laura Kovács, Andrei Voronkov:
Experimenting with SAT Solvers in Vampire. MICAI (1) 2014: 431-442 - [c89]Armin Biere:
Lingeling Essentials, A Tutorial on Design and Implementation Aspects of the the SAT Solver Lingeling. POS@SAT 2014: 88 - [c88]Andreas Fröhlich, Gergely Kovásznai, Armin Biere, Helmut Veith:
iDQ: Instantiation-Based DQBF Solving. POS@SAT 2014: 103-116 - [c87]Armin Biere, Daniel Le Berre, Emmanuel Lonca, Norbert Manthey:
Detecting Cardinality Constraints in CNF. SAT 2014: 285-301 - [c86]Adrian Balint, Armin Biere, Andreas Fröhlich, Uwe Schöning:
Improving Implementation of SLS Solvers for SAT and New Heuristics for k-SAT with Long Clauses. SAT 2014: 302-316 - [c85]Tomás Balyo, Andreas Fröhlich, Marijn Heule, Armin Biere:
Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask). SAT 2014: 317-332 - [e10]Armin Biere, Roderick Bloem:
Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. Lecture Notes in Computer Science 8559, Springer 2014, ISBN 978-3-319-08866-2 [contents] - [i3]Peter van der Tak, Marijn Heule, Armin Biere:
Concurrent Cube-and-Conquer. CoRR abs/1402.4465 (2014) - 2013
- [c84]Armin Biere, Jens Knoop, Laura Kovács, Jakob Zwirchmayr:
SmacC: A Retargetable Symbolic Execution Engine. ATVA 2013: 482-486 - [c83]Gergely Kovásznai, Andreas Fröhlich, Armin Biere:
: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into. CADE 2013: 443-449 - [c82]Marijn Heule