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
- 2024
[j34]Muhammad Osama
, Anton Wijs, Armin Biere:
Certified SAT solving with GPU accelerated inprocessing. Formal Methods Syst. Des. 62(1): 79-118 (2024)- [c179]Giuseppe Spallitta, Roberto Sebastiani, Armin Biere:
Disjoint Partial Enumeration without Blocking Clauses. AAAI 2024: 8126-8135 - [c178]Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, Florian Pollitt:
CaDiCaL 2.0. CAV (1) 2024: 133-152 - [c177]Cunjing Ge, Armin Biere:
Improved Bounds of Integer Solution Counts via Volume and Extending to Mixed-Integer Linear Constraints. CP 2024: 13:1-13:17 - [c176]Nils Froleyks, Emily Yu, Armin Biere, Keijo Heljanko:
Certifying Phase Abstraction. IJCAR (1) 2024: 284-303 - [c175]Katalin Fazekas, Florian Pollitt, Mathias Fleury, Armin Biere:
Certifying Incremental SAT Solving. LPAR 2024: 321-340 - [c174]Armin Biere, Katalin Fazekas, Mathias Fleury, Nils Froleyks:
Clausal Congruence Closure. SAT 2024: 6:1-6:25 - [c173]Jean-Marie Lagniez, Pierre Marquis, Armin Biere:
Dynamic Blocked Clause Elimination for Projected Model Counting. SAT 2024: 21:1-21:17 - [i14]Nils Froleyks, Emily Yu, Armin Biere, Keijo Heljanko:
Certifying Phase Abstraction. CoRR abs/2405.04297 (2024) - [i13]Jean-Marie Lagniez, Pierre Marquis, Armin Biere:
Dynamic Blocked Clause Elimination for Projected Model Counting. CoRR abs/2408.06199 (2024) - 2023
- [j33]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) - [c172]Emily Yu, Nils Froleyks, Armin Biere, Keijo Heljanko:
Towards Compositional Hardware Model Checking Certification. FMCAD 2023: 1-11 - [c171]Nils Froleyks, Emily Yu, Armin Biere:
BIG Backbones. FMCAD 2023: 162-167 - [c170]Armin Biere, Nils Froleyks, Wenxi Wang:
CadiBack: Extracting Backbones with CaDiCaL. SAT 2023: 3:1-3:12 - [c169]Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere:
IPASIR-UP: User Propagators for CDCL. SAT 2023: 8:1-8:13 - [c168]Florian Pollitt, Mathias Fleury, Armin Biere:
Faster LRAT Checking Than Solving with CaDiCaL. SAT 2023: 21:1-21:12 - [c167]Tobias Paxian, Armin Biere:
Uncovering and Classifying Bugs in MaxSAT Solvers through Fuzzing and Delta Debugging. POS@SAT 2023: 59-71 - [c166]Armin Biere, Mathias Fleury, Nils Froleyks, Marijn J. H. Heule:
The SAT Museum. POS@SAT 2023: 72-87 - [c165]Maximilian Heisinger, Martina Seidl, Armin Biere:
ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving. TACAS (1) 2023: 426-447 - [d2]Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere:
Supplementary material of submission "IPASIR-UP: User Propagators for CDCL". Zenodo, 2023
- [i12]Giuseppe Spallitta, Roberto Sebastiani, Armin Biere:
Enumerating Disjoint Partial Models without Blocking Clauses. CoRR abs/2306.00461 (2023) - 2022
- [j32]Mathias Fleury, Armin Biere:
Mining definitions in Kissat with Kittens. Formal Methods Syst. Des. 60(3): 381-404 (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 - [d1]Maximilian Heisinger, Martina Seidl, Armin Biere:
Artifact for Paper ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving. Zenodo, 2022 - [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, Matti Järvisalo, Armin Biere:
Revisiting Hyper Binary Resolution. CPAIOR 2013: 77-93 - [c81]Andreas Fröhlich, Gergely Kovásznai, Armin Biere:
More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics with Binary Encoding. CSR 2013: 378-390 - [c80]Alexandra Goultiaeva, Martina Seidl, Armin Biere:
Bridging the gap between dual propagation and CNF-based QBF solving. DATE 2013: 811-814 - [c79]Mathias Preiner, Aina Niemetz, Armin Biere:
Lemmas on Demand for Lambdas. DIFTS@FMCAD 2013 - [c78]Cyrille Valentin Artho, Armin Biere, Masami Hagiya, Eric Platon, Martina Seidl, Yoshinori Tanabe, Mitsuharu Yamamoto:
Modbat: A Model-Based API Tester for Event-Driven Systems. Haifa Verification Conference 2013: 112-128 - [c77]Marijn Heule, Armin Biere:
Blocked Clause Decomposition. LPAR 2013: 423-438 - [c76]Martin Aigner, Armin Biere, Christoph M. Kirsch, Aina Niemetz, Mathias Preiner:
Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures. POS@SAT 2013: 28-40 - [c75]Jean-Marie Lagniez, Armin Biere:
Factoring Out Assumptions to Speed Up MUS Extraction. SAT 2013: 276-292 - [c74]Cyrille Artho, Armin Biere, Martina Seidl:
Model-Based Testing for Verification Back-Ends. TAP@STAF 2013: 39-55 - [c73]Armin Biere, Jens Knoop, Laura Kovács, Jakob Zwirchmayr:
The Auspicious Couple: Symbolic Execution and WCET Analysis. WCET 2013: 53-63 - [e9]Armin Biere, Amir Nahir, Tanja E. J. Vos:
Hardware and Software: Verification and Testing - 8th International Haifa Verification Conference, HVC 2012, Haifa, Israel, November 6-8, 2012. Revised Selected Papers. Lecture Notes in Computer Science 7857, Springer 2013, ISBN 978-3-642-39610-6 [contents] - 2012
- [j16]Matti Järvisalo, Armin Biere, Marijn Heule:
Simulating Circuit-Level Simplifications on CNF. J. Autom. Reason. 49(4): 583-619 (2012) - [c72]Armin Biere:
Practical Aspects of SAT Solving. SMT@IJCAR 2012: 1 - [c71]Armin Biere:
Practical Aspects of SAT Solving. PAAR@IJCAR 2012: 1 - [c70]Gergely Kovásznai, Andreas Fröhlich, Armin Biere:
On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width. SMT@IJCAR 2012: 44-56 - [c69]Martina Seidl, Florian Lonsing, Armin Biere:
qbf2epr: A Tool for Generating EPR Formulas from QBF. PAAR@IJCAR 2012: 139-148 - [c68]Matti Järvisalo, Marijn Heule, Armin Biere:
Inprocessing Rules. IJCAR 2012: 355-370 - [c67]Norbert Manthey, Marijn Heule, Armin Biere:
Automated Reencoding of Boolean Formulas. Haifa Verification Conference 2012: 102-117 - [c66]Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, Armin Biere:
Resolution-Based Certificate Extraction for QBF - (Tool Presentation). SAT 2012: 430-435 - [c65]Peter van der Tak, Marijn Heule, Armin Biere:
Concurrent Cube-and-Conquer - (Poster Presentation). SAT 2012: 475-476 - [c64]Magdalena Widl, Armin Biere, Petra Brosch, Uwe Egly, Marijn Heule, Gerti Kappel, Martina Seidl, Hans Tompits:
Guided Merging of Sequence Diagrams. SLE 2012: 164-183 - [c63]Alexander Nöhrer, Armin Biere, Alexander Egyed:
A comparison of strategies for tolerating inconsistencies during decision-making. SPLC (1) 2012: 11-20 - [c62]Alexander Nöhrer, Armin Biere, Alexander Egyed:
Managing SAT inconsistencies with HUMUS. VaMoS 2012: 83-91 - [e8]Vladimir Klebanov, Bernhard Beckert, Armin Biere, Geoff Sutcliffe:
Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, Manchester, United Kingdom, June 30, 2012. CEUR Workshop Proceedings 873, CEUR-WS.org 2012 [contents] - [e7]Malay K. Ganai, Armin Biere:
Proceedings of the First International Workshop on Design and Implementation of Formal Tools and Systems, Austin, USA, November 3, 2011. CEUR Workshop Proceedings 832, CEUR-WS.org 2012 [contents] - 2011
- [j15]Armin Biere, Karen Yorav:
Preface. Formal Methods Syst. Des. 39(2): 115-116 (2011) - [c61]Armin Biere, Florian Lonsing, Martina Seidl:
Blocked Clause Elimination for QBF. CADE 2011: 101-115 - [c60]Armin Biere:
Preprocessing and Inprocessing Techniques in SAT. Haifa Verification Conference 2011: 1 - [c59]Marijn Heule, Oliver Kullmann, Siert Wieringa, Armin Biere:
Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads. Haifa Verification Conference 2011: 50-65 - [c58]Marijn Heule, Matti Järvisalo, Armin Biere:
Efficient CNF Simplification Based on Binary Implication Graphs. SAT 2011: 201-215 - [c57]Florian Lonsing, Armin Biere:
Failed Literal Detection for QBF. SAT 2011: 259-272 - 2010
- [j14]Florian Lonsing, Armin Biere:
DepQBF: A Dependency-Aware QBF Solver. J. Satisf. Boolean Model. Comput. 7(2-3): 71-76 (2010) - [c56]Marijn Heule, Matti Järvisalo, Armin Biere:
Covered Clause Elimination. LPAR short papers(Yogyakarta) 2010: 41-46 - [c55]Marijn Heule, Matti Järvisalo, Armin Biere:
Clause Elimination Procedures for CNF Formulas. LPAR (Yogyakarta) 2010: 357-371 - [c54]Robert Brummayer, Florian Lonsing, Armin Biere:
Automated Testing and Debugging of SAT and QBF Solvers. SAT 2010: 44-57 - [c53]Florian Lonsing, Armin Biere:
Integrating Dependency Schemes in Search-Based QBF Solvers. SAT 2010: 158-171 - [c52]Matti Järvisalo, Armin Biere:
Reconstructing Solutions after Blocked Clause Elimination. SAT 2010: 340-345 - [c51]Matti Järvisalo, Armin Biere, Marijn Heule:
Blocked Clause Elimination. TACAS 2010: 129-144 - [i2]Marijn Heule, Matti Järvisalo, Armin Biere:
Covered Clause Elimination. CoRR abs/1011.5202 (2010)
2000 – 2009
- 2009
- [j13]Robert Brummayer, Armin Biere:
Lemmas on Demand for the Extensional Theory of Arrays. J. Satisf. Boolean Model. Comput. 6(1-3): 165-201 (2009) - [c50]Robert Brummayer, Armin Biere:
Effective Bit-Width and Under-Approximation. EUROCAST 2009: 304-311 - [c49]Armin Biere:
SAT, SMT and Applications. LPNMR 2009: 1 - [c48]Niklas Sörensson, Armin Biere:
Minimizing Learned Clauses. SAT 2009: 237-243 - [c47]Florian Lonsing, Armin Biere:
A Compact Representation for Syntactic Dependencies in QBFs. SAT 2009: 398-411 - [c46]Robert Brummayer, Armin Biere:
Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. TACAS 2009: 174-177 - [p1]Armin Biere:
Bounded Model Checking. Handbook of Satisfiability 2009: 457-481 - [e6]Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh:
Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications 185, IOS Press 2009, ISBN 978-1-58603-929-5 [contents] - 2008
- [j12]Armin Biere:
PicoSAT Essentials. J. Satisf. Boolean Model. Comput. 4(2-4): 75-97 (2008) - [c45]Armin Biere:
Tutorial on Model Checking: Modelling and Verification in Computer Science. AB 2008: 16-21 - [c44]Armin Biere, Robert Brummayer:
Consistency Checking of All Different Constraints over Bit-Vectors within a SAT Solver. FMCAD 2008: 1-4 - [c43]Armin Biere:
Adaptive Restart Strategies for Conflict Driven SAT Solvers. SAT 2008: 28-33 - [c42]Florian Lonsing, Armin Biere:
Nenofex: Expanding NNF for QBF Solving. SAT 2008: 196-210 - [c41]Florian Lonsing, Armin Biere:
Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers. MEMICS 2008: 83-95 - 2007
- [c40]Robert Brummayer, Armin Biere:
C32SAT: Checking C Expressions. CAV 2007: 294-297 - [c39]Cyrille Artho, Boris Zweimüller, Armin Biere, Etsuya Shibayama, Shinichi Honiden:
Efficient Model Checking of Applications with Input/Output. EUROCAST 2007: 515-522 - [c38]Toni Jussila, Armin Biere, Carsten Sinz, Daniel Kröning, Christoph M. Wintersteiger:
A First Step Towards a Unified Proof Checker for QBF. SAT 2007: 201-214 - [e5]Ofer Strichman, Armin Biere:
Proceedings of the Fourth International Workshop on Bounded Model Checking, BMC@FLoC 2006, Seattle, WA, USA, August 15, 2006. Electronic Notes in Theoretical Computer Science 174(3), Elsevier 2007 [contents] - 2006
- [j11]Armin Biere, Carsten Sinz:
Decomposing SAT Problems into Connected Components. J. Satisf. Boolean Model. Comput. 2(1-4): 201-208 (2006) - [j10]Armin Biere, Keijo Heljanko, Tommi A. Junttila, Timo Latvala, Viktor Schuppan:
Linear Encodings of Bounded LTL Model Checking. Log. Methods Comput. Sci. 2(5) (2006) - [c37]Carsten Sinz, Armin Biere:
Extended Resolution Proofs for Conjoining BDDs. CSR 2006: 600-611 - [c36]Cyrille Artho, Armin Biere, Shinichi Honiden:
Enforcer - Efficient Failure Injection. FM 2006: 412-427 - [c35]Cyrille Artho, Armin Biere, Shinichi Honiden:
Exhaustive Testing of Exception Handlers with Enforcer. FMCO 2006: 26-46 - [c34]Cyrille Artho, Armin Biere:
Advanced Unit Testing: How to Scale up a Unit Test Framework. AST 2006: 92-98 - [c33]Toni Jussila, Carsten Sinz, Armin Biere:
Extended Resolution Proofs for Symbolic SAT Solving with Quantification. SAT 2006: 54-60 - [c32]Ofer Strichman, Armin Biere:
Preface. BMC@FLoC 2006: 1-2 - [c31]Toni Jussila, Armin Biere:
Compressing BMC Encodings with QBF. BMC@FLoC 2006: 45-56 - [e4]Armin Biere, Ofer Strichman:
Proceedings of the Third International Workshop on Bounded Model Checking, BMC@CAV 2005, Edinburgh, UK, July 11, 2005. Electronic Notes in Theoretical Computer Science 144(1), Elsevier 2006 [contents] - [e3]Armin Biere, Carla P. Gomes:
Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings. Lecture Notes in Computer Science 4121, Springer 2006, ISBN 3-540-37206-7 [contents] - [i1]Armin Biere, Keijo Heljanko, Tommi A. Junttila, Timo Latvala, Viktor Schuppan:
Linear Encodings of Bounded LTL Model Checking. CoRR abs/cs/0611029 (2006) - 2005
- [j9]Armin Biere, Ofer Strichman:
Introductory paper. Int. J. Softw. Tools Technol. Transf. 7(2): 87-88 (2005) - [j8]Mukul R. Prasad, Armin Biere, Aarti Gupta:
A survey of recent advances in SAT-based formal verification. Int. J. Softw. Tools Technol. Transf. 7(2): 156-173 (2005) - [c30]Niklas Eén, Armin Biere:
Effective Preprocessing in SAT Through Variable and Clause Elimination. SAT 2005: 61-75 - [c29]Malek Haroud, Armin Biere:
SDL Versus C Equivalence Checking. SDL Forum 2005: 323-338 - [c28]Viktor Schuppan, Armin Biere:
Shortest Counterexamples for Symbolic Model Checking of LTL with Past. TACAS 2005: 493-509 - [c27]Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila:
Simple Is Better: Efficient Bounded Model Checking for Past LTL. VMCAI 2005: 380-395 - [c26]Armin Biere, Ofer Strichman:
Preface. BMC@CAV 2005: 1 - [c25]Cyrille Artho, Armin Biere:
Combined Static and Dynamic Analysis. AIOOL@VMCAI 2005: 3-14 - [c24]Viktor Schuppan, Armin Biere:
Liveness Checking as Safety Checking for Infinite State Spaces. INFINITY 2005: 79-96 - [c23]Cyrille Artho, Armin Biere:
Subroutine Inlining and Bytecode Abstraction to Simplify Static and Dynamic Analysis. Bytecode@ETAPS 2005: 109-128 - [e2]Armin Biere, Ofer Strichman:
Proceedings of the 2nd International Workshop on Bounded Model Checking, BMC@CAV 2004, Boston, MA, USA, July 18, 2004. Electronic Notes in Theoretical Computer Science 119(2), Elsevier 2005 [contents] - 2004
- [j7]Viktor Schuppan, Armin Biere:
Efficient reduction of finite state model checking to reachability analysis. Int. J. Softw. Tools Technol. Transf. 5(2-3): 185-204 (2004) - [c22]Cyrille Artho, Klaus Havelund, Armin Biere:
Using Block-Local Atomicity to Detect Stale-Value Concurrency Errors. ATVA 2004: 150-164 - [c21]Cyrille Artho, Viktor Schuppan, Armin Biere, Pascal Eugster, Marcel Baur, Boris Zweimüller:
JNuke: Efficient Dynamic Analysis for Java. CAV 2004: 462-465 - [c20]Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila:
Simple Bounded LTL Model Checking. FMCAD 2004: 186-200 - [c19]Armin Biere:
Resolve and Expand. SAT 2004 - [c18]Armin Biere:
Resolve and Expand. SAT (Selected Papers 2004: 59-70 - [c17]Armin Biere, Ofer Strichman:
Preface. BMC@CAV 2004: 1- - [c16]Viktor Schuppan, Marcel Baur, Armin Biere:
JVM Independent Replay in Java. RV@ETAPS 2004: 85-104 - 2003
- [j6]Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, Yunshan Zhu:
Bounded model checking. Adv. Comput. 58: 117-148 (2003) - [j5]David A. Plaisted, Armin Biere, Yunshan Zhu:
A satisfiability procedure for quantified Boolean formulae. Discret. Appl. Math. 130(2): 291-328 (2003) - [j4]Viktor Schuppan, Armin Biere:
Verifying the IEEE 1394 FireWire Tree Identify Protocol with SMV. Formal Aspects Comput. 14(3): 267-280 (2003) - [j3]Cyrille Artho, Klaus Havelund, Armin Biere:
High-level data races. Softw. Test. Verification Reliab. 13(4): 207-227 (2003) - [c15]Cyrille Artho, Klaus Havelund, Armin Biere:
High-Level Data Races. NDDL/VVEIS 2003: 82-93 - [c14]Armin Biere, Cyrille Artho, Malek Haroud, Viktor Schuppan:
Formal Methods Group ETH Zürich. FMICS 2003: 289-293 - [c13]Ofer Strichman, Armin Biere:
Preface. BMC@CAV 2003: 541-542 - [e1]Ofer Strichman, Armin Biere:
First International Workshop on Bounded Model Checking, BMC@CAV 2003, Boulder, Colorado, USA, July 13, 2003. Electronic Notes in Theoretical Computer Science 89(4), Elsevier 2003 [contents] - 2002
- [j2]Sergey Berezin, Edmund M. Clarke, Armin Biere, Yunshan Zhu:
Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function. Formal Methods Syst. Des. 20(2): 159-186 (2002) - [c12]Armin Biere, Wolfgang Kunz:
SAT and ATPG: Boolean engines for formal hardware verification. ICCAD 2002: 782-785 - [c11]Armin Biere, Cyrille Artho, Viktor Schuppan:
Liveness Checking as Safety Checking. FMICS 2002: 160-177 - 2001
- [j1]Edmund M. Clarke, Armin Biere, Richard Raimi, Yunshan Zhu:
Bounded Model Checking Using Satisfiability Solving. Formal Methods Syst. Des. 19(1): 7-34 (2001) - [c10]Cyrille Artho, Armin Biere:
Applying Static Analysis to Large-Scale, Multi-Threaded Java Programs. Australian Software Engineering Conference 2001: 68-75 - 2000
- [c9]Poul Frederick Williams, Armin Biere, Edmund M. Clarke, Anubhav Gupta:
Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. CAV 2000: 124-138
1990 – 1999
- 1999
- [c8]Armin Biere, Edmund M. Clarke, Yunshan Zhu:
Multiple State and Single State Tableaux for Combining Local and Global Model Checking. Correct System Design 1999: 163-179 - [c7]Armin Biere, Edmund M. Clarke, Richard Raimi, Yunshan Zhu:
Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs. CAV 1999: 60-71 - [c6]Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Masahiro Fujita, Yunshan Zhu:
Symbolic Model Checking Using SAT Procedures instead of BDDs. DAC 1999: 317-320 - [c5]Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu:
Symbolic Model Checking without BDDs. TACAS 1999: 193-207 - [c4]Armin Biere, Edmund M. Clarke, Yunshan Zhu:
Combining Local and Global Model Checking. SMC@FLoC 1999: 34-45 - 1998
- [c3]Bwolen Yang, Randal E. Bryant, David R. O'Hallaron, Armin Biere, Olivier Coudert, Geert Janssen, Rajeev K. Ranjan, Fabio Somenzi:
A Performance Study of BDD-Based Model Checking. FMCAD 1998: 255-289 - [c2]Sergey Berezin, Armin Biere, Edmund M. Clarke, Yunshan Zhu:
Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification. FMCAD 1998: 369-386 - 1997
- [b1]Armin Biere:
Effiziente Modellprüfung des µ-Kalküls mit binären Entscheidungsdiagrammen. Universität Karlsruhe, 1997, pp. I-VIII, 1-230 - [c1]Armin Biere:
µcke - Efficient µ-Calculus Model Checking. CAV 1997: 468-471
Coauthor Index
Cyrille Artho
aka: Cyrille Valentin Artho
aka: Cyrille Valentin Artho
Nils Christian Froleyks
aka: Nils Froleyks
aka: Nils Froleyks
Marijn Heule
aka: Marijn J. H. Heule
aka: Marijn J. H. Heule
Daniela Kaufmann
aka: Daniela Ritirc
aka: Daniela Ritirc
Benjamin Kiesl-Reiter
aka: Benjamin Kiesl
aka: Benjamin Kiesl
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-31 21:07 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
