Armin Biere - RankMe

261 papers A* 12A 54B 39C 3Misc 4Journal 56Unranked 76

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	MaxSAT Fuzzing and Delta Debugging. J. Artif. Intell. Res. Tobias Paxian, Armin Biere
2026	—	`conf`	Real-time Proof Checking for Distributed Incremental SAT Solving. TACAS (1) Dominik Schreiber, Mathias Fleury, Katalin Fazekas, Armin Biere
2025	J	`jnl`	Disjoint projected enumeration for SAT and SMT without blocking clauses. Artif. Intell. Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
2025	B	`conf`	Hardware Model Checking Competition 2025. FMCAD Armin Biere, Nils Froleyks, Mathias Preiner
2025	—	`conf`	Introducing Certificates to the Hardware Model Checking Competition. CAV (1) Nils Froleyks, Emily Yu, Mathias Preiner, Armin Biere, Keijo Heljanko
2025	A	`conf`	Learn to Unlearn. SAT Bernhard Gstrein, Florian Pollitt, André Schidler, Mathias Fleury, Armin Biere
2025	J	`jnl`	On enumerating short projected models. Discret. Appl. Math. Sibylle Möhle, Roberto Sebastiani, Armin Biere
2025	J	`jnl`	SAT solving for variants of first-order subsumption. Formal Methods Syst. Des. Robin Coutelier, Jakob Rath, Michael Rawson, Armin Biere, Laura Kovács
2025	A	`conf`	Streamlining Distributed SAT Solver Design. SAT Dominik Schreiber, Niccolò Rigi-Luperti, Armin Biere
2024	—	`conf`	CaDiCaL 2.0. CAV (1) Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, Florian Pollitt
2024	J	`jnl`	Certified SAT solving with GPU accelerated inprocessing. Formal Methods Syst. Des. Muhammad Osama, Anton Wijs, Armin Biere
2024	B	`conf`	Certifying Incremental SAT Solving. LPAR Katalin Fazekas, Florian Pollitt, Mathias Fleury, Armin Biere
2024	—	`conf`	Certifying Phase Abstraction. IJCAR (1) Nils Froleyks, Emily Yu, Armin Biere, Keijo Heljanko
2024	J	`jnl`	Certifying Phase Abstraction. CoRR Nils Froleyks, Emily Yu, Armin Biere, Keijo Heljanko
2024	A	`conf`	Clausal Congruence Closure. SAT Armin Biere, Katalin Fazekas, Mathias Fleury, Nils Froleyks
2024	B	`conf`	Clausal Equivalence Sweeping. FMCAD Armin Biere, Katalin Fazekas, Mathias Fleury, Nils Froleyks
2024	A*	`conf`	Disjoint Partial Enumeration without Blocking Clauses. AAAI Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
2024	J	`jnl`	Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses. CoRR Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
2024	A	`conf`	Dynamic Blocked Clause Elimination for Projected Model Counting. SAT Jean-Marie Lagniez, Pierre Marquis, Armin Biere
2024	J	`jnl`	Dynamic Blocked Clause Elimination for Projected Model Counting. CoRR Jean-Marie Lagniez, Pierre Marquis, Armin Biere
2024	B	`conf`	Hardware Model Checking Competition 2024. FMCAD Armin Biere, Nils Froleyks, Mathias Preiner
2024	A	`conf`	Improved Bounds of Integer Solution Counts via Volume and Extending to Mixed-Integer Linear Constraints. CP Cunjing Ge, Armin Biere
2024	J	`jnl`	Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker. Formal Methods Syst. Des. Daniela Kaufmann, Mathias Fleury, Armin Biere, Manuel Kauers
2024	J	`jnl`	SAT Solving for Variants of First-Order Subsumption. CoRR Robin Coutelier, Jakob Rath, Michael Rawson, Armin Biere, Laura Kovács
2024	J	`jnl`	Satisfiability Modulo User Propagators. J. Artif. Intell. Res. Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere
2023	B	`conf`	BIG Backbones. FMCAD Nils Froleyks, Emily Yu, Armin Biere
2023	A	`conf`	CadiBack: Extracting Backbones with CaDiCaL. SAT Armin Biere, Nils Froleyks, Wenxi Wang
2023	J	`jnl`	Enumerating Disjoint Partial Models without Blocking Clauses. CoRR Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
2023	A	`conf`	Faster LRAT Checking Than Solving with CaDiCaL. SAT Florian Pollitt, Mathias Fleury, Armin Biere
2023	A	`conf`	IPASIR-UP: User Propagators for CDCL. SAT Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere
2023	J	`jnl`	Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra. Int. J. Softw. Tools Technol. Transf. Daniela Kaufmann, Armin Biere
2023	—	`conf`	ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving. TACAS (1) Maximilian Heisinger, Martina Seidl, Armin Biere
2023	—	`conf`	The SAT Museum. POS@SAT Armin Biere, Mathias Fleury, Nils Froleyks, Marijn J. H. Heule
2023	B	`conf`	Towards Compositional Hardware Model Checking Certification. FMCAD Emily Yu, Nils Froleyks, Armin Biere, Keijo Heljanko
2023	—	`conf`	Uncovering and Classifying Bugs in MaxSAT Solvers through Fuzzing and Delta Debugging. POS@SAT Tobias Paxian, Armin Biere
2022	A	`conf`	Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification. DATE Daniela Kaufmann, Paul Beame, Armin Biere, Jakob Nordström
2022	J	`jnl`	Better Decision Heuristics in CDCL through Local Search and Target Phases. J. Artif. Intell. Res. Shaowei Cai, Xindi Zhang, Mathias Fleury, Armin Biere
2022	—	`conf`	Clausal Proofs for Pseudo-Boolean Reasoning. TACAS (1) Randal E. Bryant, Armin Biere, Marijn J. H. Heule
2022	B	`conf`	First-Order Subsumption via SAT Solving. FMCAD Jakob Rath, Armin Biere, Laura Kovács
2022	—	`conf`	Fuzzing and Delta Debugging And-Inverter Graph Verification Tools. TAP@STAF Daniela Kaufmann, Armin Biere
2022	A	`conf`	Migrating Solver State. SAT Armin Biere, Md. Solimul Chowdhury, Marijn J. H. Heule, Benjamin Kiesl, Michael W. Whalen
2022	J	`jnl`	Mining definitions in Kissat with Kittens. Formal Methods Syst. Des. Mathias Fleury, Armin Biere
2022	—	`conf`	QuAPI: Adding Assumptions to Non-Assuming SAT & QBF Solvers. PAAR@IJCAR Maximilian Heisinger, Martina Seidl, Armin Biere
2022	J	`jnl`	Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses. CoRR Mathias Fleury, Armin Biere
2022	B	`conf`	Stratified Certification for k-Induction. FMCAD Emily Yu, Nils Froleyks, Armin Biere, Keijo Heljanko
2022	J	`jnl`	Stratified Certification for k-Induction. CoRR Emily Yu, Nils Froleyks, Armin Biere, Keijo Heljanko
2022	J	`jnl`	Theory and Practice of SAT and Combinatorial Solving (Dagstuhl Seminar 22411). Dagstuhl Reports Olaf Beyersdorff, Armin Biere, Vijay Ganesh, Jakob Nordström, Andy Oertel
2022	J	`jnl`	Tools and algorithms for the construction and analysis of systems: a special issue for TACAS 2020. Int. J. Softw. Tools Technol. Transf. Armin Biere, David Parker
2021	—	`conf`	AMulet 2.0 for Verifying Multiplier Circuits. TACAS (2) Daniela Kaufmann, Armin Biere
2021	—	`ch.`	Bounded Model Checking. Handbook of Satisfiability Armin Biere
2021	A*	`conf`	Decomposition Strategies to Count Integer Solutions over Linear Constraints. IJCAI Cunjing Ge, Armin Biere
2021	A	`conf`	Efficient All-UIP Learned Clause Minimization. SAT Mathias Fleury, Armin Biere
2021	—	`book`	Handbook of Satisfiability - Second Edition Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh
2021	A	`conf`	Non-clausal Redundancy Properties. CADE Lee A. Barnett, Armin Biere
2021	J	`jnl`	On Enumerating Short Projected Models. CoRR Sibylle Möhle, Roberto Sebastiani, Armin Biere
2021	—	`ch.`	Preprocessing in SAT Solving. Handbook of Satisfiability Armin Biere, Matti Järvisalo, Benjamin Kiesl
2021	—	`conf`	Progress in Certifying Hardware Model Checking Results. CAV (2) Emily Yu, Armin Biere, Keijo Heljanko
2021	—	`conf`	SAT Solving with GPU Accelerated Inprocessing. TACAS (1) Muhammad Osama, Anton Wijs, Armin Biere
2021	B	`conf`	Single Clause Assumption without Activation Literals to Speed-up IC3. FMCAD Nils Froleyks, Armin Biere
2021	A	`conf`	XOR Local Search for Boolean Brent Equations. SAT Wojciech Nawrocki, Zhenjun Liu, Andreas Fröhlich, Marijn J. H. Heule, Armin Biere
2020	B	`conf`	Aiding an Introduction to Formal Reasoning Within a First-Year Logic Course for CS Majors Using a Mobile Self-Study App. ITiCSE David M. Cerna, Martina Seidl, Wolfgang Schreiner, Wolfgang Windsteiger, Armin Biere
2020	—	`conf`	Computational Logic in the First Semester of Computer Science: An Experience Report. CSEDU (2) David M. Cerna, Martina Seidl, Wolfgang Schreiner, Wolfgang Windsteiger, Armin Biere
2020	—	`conf`	Covered Clauses Are Not Propagation Redundant. IJCAR (1) Lee A. Barnett, David M. Cerna, Armin Biere
2020	A	`conf`	Distributed Cube and Conquer with Paracooba. SAT Maximilian Heisinger, Mathias Fleury, Armin Biere
2020	B	`conf`	Duplex Encoding of Staircase At-Most-One Constraints for the Antibandwidth Problem. CPAIOR Katalin Fazekas, Markus Sinnl, Armin Biere, Sophie N. Parragh
2020	A	`conf`	Four Flavors of Entailment. SAT Sibylle Möhle, Roberto Sebastiani, Armin Biere
2020	A	`conf`	From DRUP to PAC and Back. DATE Daniela Kaufmann, Armin Biere, Manuel Kauers
2020	J	`jnl`	Incremental column-wise verification of arithmetic circuits using computer algebra. Formal Methods Syst. Des. Daniela Kaufmann, Armin Biere, Manuel Kauers
2020	B	`conf`	Nullstellensatz-Proofs for Multiplier Verification. CASC Daniela Kaufmann, Armin Biere
2020	J	`jnl`	Preface to the Special Issue on Automated Reasoning Systems. J. Autom. Reason. Armin Biere, Cesare Tinelli, Christoph Weidenbach
2020	J	`jnl`	Simulating Strong Practical Proof Systems with Extended Resolution. J. Autom. Reason. Benjamin Kiesl, Adrián Rebola-Pardo, Marijn J. H. Heule, Armin Biere
2020	J	`jnl`	Strong Extension-Free Proof Systems. J. Autom. Reason. Marijn J. H. Heule, Benjamin Kiesl, Armin Biere
2020	B	`conf`	The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus. FMCAD Daniela Kaufmann, Mathias Fleury, Armin Biere
2020	—	`ed.`	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 TACAS (1) Armin Biere, David Parker
2020	—	`ed.`	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 TACAS (2) Armin Biere, David Parker
2020	B	`conf`	Tutorial on World-Level Model Checking. FMCAD Armin Biere
2019	—	`conf`	A Framework for Model Checking Against CTLK Using Quantified Boolean Formulas. FTSCS Emily Yu, Martina Seidl, Armin Biere
2019	B	`conf`	A Survey on Applications of Quantified Boolean Formulas. ICTAI Ankit Shukla, Armin Biere, Luca Pulina, Martina Seidl
2019	A	`conf`	Backing Backtracking. SAT Sibylle Möhle, Armin Biere
2019	C	`conf`	Certifying Hardware Model Checking Results. ICFEM Zhengqi Yu, Armin Biere, Keijo Heljanko
2019	—	`conf`	Clausal Proofs of Mutilated Chessboards. NFM Marijn J. H. Heule, Benjamin Kiesl, Armin Biere
2019	—	`conf`	Combining Conflict-Driven Clause Learning and Chronological Backtracking for Propositional Model Counting. GCAI Sibylle Möhle, Armin Biere
2019	—	`conf`	Encoding Redundancy for Satisfaction-Driven Clause Learning. TACAS (1) Marijn J. H. Heule, Benjamin Kiesl, Armin Biere
2019	A	`conf`	Incremental Inprocessing in SAT Solving. SAT Katalin Fazekas, Armin Biere, Christoph Scholl
2019	—	`conf`	SAT, Computer Algebra, Multipliers. Vampire Daniela Ritirc, Armin Biere, Manuel Kauers
2019	B	`conf`	Truth Assignments as Conditional Autarkies. ATVA Benjamin Kiesl, Marijn J. H. Heule, Armin Biere
2019	B	`conf`	Verifying Large Multipliers by Combining SAT and Computer Algebra. FMCAD Daniela Kaufmann, Armin Biere, Manuel Kauers
2018	—	`conf`	A Practical Polynomial Calculus for Arithmetic Circuit Verification. SC-Square@FLOC Daniela Ritirc, Armin Biere, Manuel Kauers
2018	—	`conf`	Btor2 , BtorMC and Boolector 3.0. CAV (1) Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere
2018	—	`ch.`	Cube-and-Conquer for Satisfiability. Handbook of Parallel Constraint Reasoning Marijn J. H. Heule, Oliver Kullmann, Armin Biere
2018	B	`conf`	Dualizing Projected Model Counting. ICTAI Sibylle Möhle, Armin Biere
2018	—	`conf`	Evaluating CDCL Restart Schemes. POS@SAT Armin Biere, Andreas Fröhlich
2018	A	`conf`	Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories. IJCAR Katalin Fazekas, Fahiem Bacchus, Armin Biere
2018	A	`conf`	Improving and extending the algebraic approach for verifying gate-level multipliers. DATE Daniela Ritirc, Armin Biere, Manuel Kauers
2018	J	`jnl`	Local Redundancy in SAT: Generalizations of Blocked Clauses. Log. Methods Comput. Sci. Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere
2018	J	`jnl`	Revisiting Decision Diagrams for SAT. CoRR Tom van Dijk, Rüdiger Ehlers, Armin Biere
2018	—	`ch.`	SAT-Based Model Checking. Handbook of Model Checking Armin Biere, Daniel Kröning
2018	—	`conf`	The Effect of Scrambling CNFs. POS@SAT Armin Biere, Marijn Heule
2018	—	`conf`	Two flavors of DRAT. POS@SAT Adrián Rebola-Pardo, Armin Biere
2018	—	`conf`	What a Difference a Variable Makes. TACAS (2) Marijn J. H. Heule, Armin Biere
2017	—	`conf`	An Abstract Dual Propositional Model Counter. YSIP Armin Biere, Steffen Hölldobler, Sibylle Möhle
2017	B	`conf`	Blocked Clauses in First-Order Logic. LPAR Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere
2017	J	`jnl`	Blocked Clauses in First-Order Logic. CoRR Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere
2017	A*	`conf`	Blockedness in Propositional Logic: Are You Satisfied With Your Neighborhood? IJCAI Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere
2017	Misc	`conf`	Challenges in Verifying Arithmetic Circuits Using Computer Algebra. SYNASC Armin Biere, Manuel Kauers, Daniela Ritirc
2017	B	`conf`	Column-wise verification of multipliers using computer algebra. FMCAD Daniela Ritirc, Armin Biere, Manuel Kauers
2017	—	`conf`	Counterexample-Guided Model Synthesis. TACAS (1) Mathias Preiner, Aina Niemetz, Armin Biere
2017	B	`conf`	Hardware model checking competition 2017. FMCAD Armin Biere, Tom van Dijk, Keijo Heljanko
2017	J	`jnl`	Local Redundancy in SAT: Generalizations of Blocked Clauses. CoRR Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere
2017	—	`conf`	Model-Based API Testing for SMT Solvers. SMT Aina Niemetz, Mathias Preiner, Armin Biere
2017	—	`conf`	PRuning Through Satisfaction. Haifa Verification Conference Marijn J. H. Heule, Benjamin Kiesl, Martina Seidl, Armin Biere
2017	J	`jnl`	Propagation based local search for bit-precise reasoning. Formal Methods Syst. Des. Aina Niemetz, Mathias Preiner, Armin Biere
2017	A	`conf`	Short Proofs Without New Variables. CADE Marijn J. H. Heule, Benjamin Kiesl, Armin Biere
2017	—	`conf`	Skolem Function Continuation for Quantified Boolean Formulas. TAP@STAF Katalin Fazekas, Marijn J. H. Heule, Martina Seidl, Armin Biere
2017	J	`jnl`	Solution Validation and Extraction for QBF Preprocessing. J. Autom. Reason. Marijn J. H. Heule, Martina Seidl, Armin Biere
2016	Misc	`conf`	A Duality-Aware Calculus for Quantified Boolean Formulas. SYNASC Katalin Fazekas, Martina Seidl, Armin Biere
2016	J	`jnl`	Complexity of Fixed-Size Bit-Vector Logics. Theory Comput. Syst. Gergely Kovásznai, Andreas Fröhlich, Armin Biere
2016	A*	`conf`	Greedy combinatorial test case generation using unsatisfiable cores. ASE Akihisa Yamada, Armin Biere, Cyrille Artho, Takashi Kitamura, Eun-Hye Choi
2016	—	`conf`	Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories. CAV (1) Aina Niemetz, Mathias Preiner, Armin Biere
2016	J	`jnl`	SAT Race 2015. Artif. Intell. Tomás Balyo, Armin Biere, Ashlin Iser, Carsten Sinz
2016	A	`conf`	Super-Blocked Clauses. IJCAR Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere
2015	B	`conf`	Better Lemmas with Lambda Extraction. FMCAD Mathias Preiner, Aina Niemetz, Armin Biere
2015	—	`conf`	Blocked Literals Are Universal. NFM Marijn Heule, Martina Seidl, Armin Biere
2015	—	`conf`	Clausal Proof Compression. IWIL@LPAR Marijn Heule, Armin Biere
2015	J	`jnl`	Clause Elimination for SAT and QSAT. J. Artif. Intell. Res. Marijn Heule, Matti Järvisalo, Florian Lonsing, Martina Seidl, Armin Biere
2015	B	`conf`	Compositional Propositional Proofs. LPAR Marijn J. H. Heule, Armin Biere
2015	B	`conf`	Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination. LPAR Florian Lonsing, Fahiem Bacchus, Armin Biere, Uwe Egly, Martina Seidl
2015	A	`conf`	Evaluating CDCL Variable Scoring Schemes. SAT Armin Biere, Andreas Fröhlich
2015	A	`conf`	Optimization of Combinatorial Testing by Incremental SAT Solving. ICST Akihisa Yamada, Takashi Kitamura, Cyrille Artho, Eun-Hye Choi, Yutaka Oiwa, Armin Biere
2015	A*	`conf`	Stochastic Local Search for Satisfiability Modulo Theories. AAAI Andreas Fröhlich, Armin Biere, Christoph M. Wintersteiger, Youssef Hamadi
2015	J	`jnl`	Theory and Practice of SAT Solving (Dagstuhl Seminar 15171). Dagstuhl Reports Armin Biere, Vijay Ganesh, Martin Grohe, Jakob Nordström, Ryan Williams
2014	A	`conf`	A Unified Proof System for QBF Preprocessing. IJCAR Marijn Heule, Martina Seidl, Armin Biere
2014	J	`jnl`	Améliorer SAT dans le cadre incrémental. Rev. d'Intelligence Artif. Gilles Audemard, Armin Biere, Jean-Marie Lagniez, Laurent Simon
2014	J	`jnl`	Boolector 2.0. J. Satisf. Boolean Model. Comput. Aina Niemetz, Mathias Preiner, Armin Biere
2014	B	`conf`	Challenges in bit-precise reasoning. FMCAD Armin Biere
2014	A*	`ed.`	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 CAV Armin Biere, Roderick Bloem
2014	J	`jnl`	Concurrent Cube-and-Conquer. CoRR Peter van der Tak, Marijn Heule, Armin Biere
2014	A	`conf`	Detecting Cardinality Constraints in CNF. SAT Armin Biere, Daniel Le Berre, Emmanuel Lonca, Norbert Manthey
2014	B	`conf`	Efficient extraction of Skolem functions from QRAT proofs. FMCAD Marijn Heule, Martina Seidl, Armin Biere
2014	A	`conf`	Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask). SAT Tomás Balyo, Andreas Fröhlich, Marijn Heule, Armin Biere
2014	—	`conf`	Experimenting with SAT Solvers in Vampire. MICAI (1) Armin Biere, Ioan Dragan, Laura Kovács, Andrei Voronkov
2014	J	`jnl`	Hardware Model Checking Competition 2014: An Analysis and Comparison of Solvers and Benchmarks. J. Satisf. Boolean Model. Comput. Gianpiero Cabodi, Carmelo Loiacono, Marco Palena, Paolo Pasini, Denis Patti, Stefano Quer, Danilo Vendraminetto, Armin Biere, Keijo Heljanko
2014	A	`conf`	Improving Implementation of SLS Solvers for SAT and New Heuristics for k-SAT with Long Clauses. SAT Adrian Balint, Armin Biere, Andreas Fröhlich, Uwe Schöning
2014	—	`conf`	Lingeling Essentials, A Tutorial on Design and Implementation Aspects of the the SAT Solver Lingeling. POS@SAT Armin Biere
2014	—	`conf`	On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic. MFCS (2) Gergely Kovásznai, Helmut Veith, Andreas Fröhlich, Armin Biere
2014	—	`conf`	SAT solving experiments in Vampire. Vampire Workshop Armin Biere, Ioan Dragan, Laura Kovács, Andrei Voronkov
2014	B	`conf`	Turbo-charging Lemmas on demand with don't care reasoning. FMCAD Aina Niemetz, Mathias Preiner, Armin Biere
2014	—	`conf`	iDQ: Instantiation-Based DQBF Solving. POS@SAT Andreas Fröhlich, Gergely Kovásznai, Armin Biere, Helmut Veith
2013	A	`conf`	: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into. CADE Gergely Kovásznai, Andreas Fröhlich, Armin Biere
2013	—	`conf`	Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures. POS@SAT Martin Aigner, Armin Biere, Christoph M. Kirsch, Aina Niemetz, Mathias Preiner
2013	B	`conf`	Blocked Clause Decomposition. LPAR Marijn Heule, Armin Biere
2013	A	`conf`	Bridging the gap between dual propagation and CNF-based QBF solving. DATE Alexandra Goultiaeva, Martina Seidl, Armin Biere
2013	A	`conf`	Factoring Out Assumptions to Speed Up MUS Extraction. SAT Jean-Marie Lagniez, Armin Biere
2013	—	`ed.`	Hardware and Software: Verification and Testing - 8th International Haifa Verification Conference, HVC 2012, Haifa, Israel, November 6-8, 2012. Revised Selected Papers Haifa Verification Conference Armin Biere, Amir Nahir, Tanja E. J. Vos
2013	—	`conf`	Lemmas on Demand for Lambdas. DIFTS@FMCAD Mathias Preiner, Aina Niemetz, Armin Biere
2013	—	`conf`	Modbat: A Model-Based API Tester for Event-Driven Systems. Haifa Verification Conference Cyrille Valentin Artho, Armin Biere, Masami Hagiya, Eric Platon, Martina Seidl, Yoshinori Tanabe, Mitsuharu Yamamoto
2013	—	`conf`	Model-Based Testing for Verification Back-Ends. TAP@STAF Cyrille Artho, Armin Biere, Martina Seidl
2013	Misc	`conf`	More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics with Binary Encoding. CSR Andreas Fröhlich, Gergely Kovásznai, Armin Biere
2013	B	`conf`	Revisiting Hyper Binary Resolution. CPAIOR Marijn Heule, Matti Järvisalo, Armin Biere
2013	B	`conf`	SmacC: A Retargetable Symbolic Execution Engine. ATVA Armin Biere, Jens Knoop, Laura Kovács, Jakob Zwirchmayr
2013	—	`conf`	The Auspicious Couple: Symbolic Execution and WCET Analysis. WCET Armin Biere, Jens Knoop, Laura Kovács, Jakob Zwirchmayr
2012	—	`conf`	A comparison of strategies for tolerating inconsistencies during decision-making. SPLC (1) Alexander Nöhrer, Armin Biere, Alexander Egyed
2012	—	`conf`	Automated Reencoding of Boolean Formulas. Haifa Verification Conference Norbert Manthey, Marijn Heule, Armin Biere
2012	A	`conf`	Concurrent Cube-and-Conquer - (Poster Presentation). SAT Peter van der Tak, Marijn Heule, Armin Biere
2012	B	`conf`	Guided Merging of Sequence Diagrams. SLE Magdalena Widl, Armin Biere, Petra Brosch, Uwe Egly, Marijn Heule, Gerti Kappel, Martina Seidl, Hans Tompits
2012	A	`conf`	Inprocessing Rules. IJCAR Matti Järvisalo, Marijn Heule, Armin Biere
2012	—	`conf`	Managing SAT inconsistencies with HUMUS. VaMoS Alexander Nöhrer, Armin Biere, Alexander Egyed
2012	—	`conf`	On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width. SMT@IJCAR Gergely Kovásznai, Andreas Fröhlich, Armin Biere
2012	—	`conf`	Practical Aspects of SAT Solving. SMT@IJCAR Armin Biere
2012	—	`conf`	Practical Aspects of SAT Solving. PAAR@IJCAR Armin Biere
2012	—	`ed.`	Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, Manchester, United Kingdom, June 30, 2012 COMPARE Vladimir Klebanov, Bernhard Beckert, Armin Biere, Geoff Sutcliffe
2012	—	`ed.`	Proceedings of the First International Workshop on Design and Implementation of Formal Tools and Systems, Austin, USA, November 3, 2011 DIFTS@FMCAD Malay K. Ganai, Armin Biere
2012	A	`conf`	Resolution-Based Certificate Extraction for QBF - (Tool Presentation). SAT Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, Armin Biere
2012	J	`jnl`	Simulating Circuit-Level Simplifications on CNF. J. Autom. Reason. Matti Järvisalo, Armin Biere, Marijn Heule
2012	—	`conf`	qbf2epr: A Tool for Generating EPR Formulas from QBF. PAAR@IJCAR Martina Seidl, Florian Lonsing, Armin Biere
2011	A	`conf`	Blocked Clause Elimination for QBF. CADE Armin Biere, Florian Lonsing, Martina Seidl
2011	—	`conf`	Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads. Haifa Verification Conference Marijn Heule, Oliver Kullmann, Siert Wieringa, Armin Biere
2011	A	`conf`	Efficient CNF Simplification Based on Binary Implication Graphs. SAT Marijn Heule, Matti Järvisalo, Armin Biere
2011	A	`conf`	Failed Literal Detection for QBF. SAT Florian Lonsing, Armin Biere
2011	J	`jnl`	Preface. Formal Methods Syst. Des. Armin Biere, Karen Yorav
2011	—	`conf`	Preprocessing and Inprocessing Techniques in SAT. Haifa Verification Conference Armin Biere
2010	A	`conf`	Automated Testing and Debugging of SAT and QBF Solvers. SAT Robert Brummayer, Florian Lonsing, Armin Biere
2010	A	`conf`	Blocked Clause Elimination. TACAS Matti Järvisalo, Armin Biere, Marijn Heule
2010	—	`conf`	Clause Elimination Procedures for CNF Formulas. LPAR (Yogyakarta) Marijn Heule, Matti Järvisalo, Armin Biere
2010	J	`jnl`	Covered Clause Elimination CoRR Marijn Heule, Matti Järvisalo, Armin Biere
2010	—	`conf`	Covered Clause Elimination. LPAR short papers(Yogyakarta) Marijn Heule, Matti Järvisalo, Armin Biere
2010	J	`jnl`	DepQBF: A Dependency-Aware QBF Solver. J. Satisf. Boolean Model. Comput. Florian Lonsing, Armin Biere
2010	A	`conf`	Integrating Dependency Schemes in Search-Based QBF Solvers. SAT Florian Lonsing, Armin Biere
2010	A	`conf`	Reconstructing Solutions after Blocked Clause Elimination. SAT Matti Järvisalo, Armin Biere
2009	A	`conf`	A Compact Representation for Syntactic Dependencies in QBFs. SAT Florian Lonsing, Armin Biere
2009	A	`conf`	Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. TACAS Robert Brummayer, Armin Biere
2009	—	`ch.`	Bounded Model Checking. Handbook of Satisfiability Armin Biere
2009	—	`conf`	Effective Bit-Width and Under-Approximation. EUROCAST Robert Brummayer, Armin Biere
2009	—	`book`	Handbook of Satisfiability Handbook of Satisfiability Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh
2009	J	`jnl`	Lemmas on Demand for the Extensional Theory of Arrays. J. Satisf. Boolean Model. Comput. Robert Brummayer, Armin Biere
2009	A	`conf`	Minimizing Learned Clauses. SAT Niklas Sörensson, Armin Biere
2009	B	`conf`	SAT, SMT and Applications. LPNMR Armin Biere
2008	A	`conf`	Adaptive Restart Strategies for Conflict Driven SAT Solvers. SAT Armin Biere
2008	B	`conf`	Consistency Checking of All Different Constraints over Bit-Vectors within a SAT Solver. FMCAD Armin Biere, Robert Brummayer
2008	—	`conf`	Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers. MEMICS Florian Lonsing, Armin Biere
2008	A	`conf`	Nenofex: Expanding NNF for QBF Solving. SAT Florian Lonsing, Armin Biere
2008	J	`jnl`	PicoSAT Essentials. J. Satisf. Boolean Model. Comput. Armin Biere
2008	—	`conf`	Tutorial on Model Checking: Modelling and Verification in Computer Science. AB Armin Biere
2007	A	`conf`	A First Step Towards a Unified Proof Checker for QBF. SAT Toni Jussila, Armin Biere, Carsten Sinz, Daniel Kröning, Christoph M. Wintersteiger
2007	A*	`conf`	C32SAT: Checking C Expressions. CAV Robert Brummayer, Armin Biere
2007	—	`conf`	Efficient Model Checking of Applications with Input/Output. EUROCAST Cyrille Artho, Boris Zweimüller, Armin Biere, Etsuya Shibayama, Shinichi Honiden
2007	—	`ed.`	Proceedings of the Fourth International Workshop on Bounded Model Checking, BMC@FLoC 2006, Seattle, WA, USA, August 15, 2006 BMC@FLoC Ofer Strichman, Armin Biere
2006	—	`conf`	Advanced Unit Testing: How to Scale up a Unit Test Framework. AST@ICSE Cyrille Artho, Armin Biere
2006	—	`conf`	Compressing BMC Encodings with QBF. BMC@FLoC Toni Jussila, Armin Biere
2006	J	`jnl`	Decomposing SAT Problems into Connected Components. J. Satisf. Boolean Model. Comput. Armin Biere, Carsten Sinz
2006	B	`conf`	Enforcer - Efficient Failure Injection. FM Cyrille Artho, Armin Biere, Shinichi Honiden
2006	—	`conf`	Exhaustive Testing of Exception Handlers with Enforcer. FMCO Cyrille Artho, Armin Biere, Shinichi Honiden
2006	Misc	`conf`	Extended Resolution Proofs for Conjoining BDDs. CSR Carsten Sinz, Armin Biere
2006	A	`conf`	Extended Resolution Proofs for Symbolic SAT Solving with Quantification. SAT Toni Jussila, Carsten Sinz, Armin Biere
2006	J	`jnl`	Linear Encodings of Bounded LTL Model Checking CoRR Armin Biere, Keijo Heljanko, Tommi A. Junttila, Timo Latvala, Viktor Schuppan
2006	J	`jnl`	Linear Encodings of Bounded LTL Model Checking. Log. Methods Comput. Sci. Armin Biere, Keijo Heljanko, Tommi A. Junttila, Timo Latvala, Viktor Schuppan
2006	—	`conf`	Preface. BMC@FLoC Ofer Strichman, Armin Biere
2006	—	`ed.`	Proceedings of the Third International Workshop on Bounded Model Checking, BMC@CAV 2005, Edinburgh, UK, July 11, 2005 BMC@CAV Armin Biere, Ofer Strichman
2006	A	`ed.`	Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings SAT Armin Biere, Carla P. Gomes
2005	J	`jnl`	A survey of recent advances in SAT-based formal verification. Int. J. Softw. Tools Technol. Transf. Mukul R. Prasad, Armin Biere, Aarti Gupta
2005	—	`conf`	Combined Static and Dynamic Analysis. AIOOL@VMCAI Cyrille Artho, Armin Biere
2005	A	`conf`	Effective Preprocessing in SAT Through Variable and Clause Elimination. SAT Niklas Eén, Armin Biere
2005	J	`jnl`	Introductory paper. Int. J. Softw. Tools Technol. Transf. Armin Biere, Ofer Strichman
2005	—	`conf`	Liveness Checking as Safety Checking for Infinite State Spaces. INFINITY Viktor Schuppan, Armin Biere
2005	—	`conf`	Preface. BMC@CAV Armin Biere, Ofer Strichman
2005	—	`ed.`	Proceedings of the 2nd International Workshop on Bounded Model Checking, BMC@CAV 2004, Boston, MA, USA, July 18, 2004 BMC@CAV Armin Biere, Ofer Strichman
2005	—	`conf`	SDL Versus C Equivalence Checking. SDL Forum Malek Haroud, Armin Biere
2005	A	`conf`	Shortest Counterexamples for Symbolic Model Checking of LTL with Past. TACAS Viktor Schuppan, Armin Biere
2005	B	`conf`	Simple Is Better: Efficient Bounded Model Checking for Past LTL. VMCAI Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila
2005	—	`conf`	Subroutine Inlining and Bytecode Abstraction to Simplify Static and Dynamic Analysis. Bytecode@ETAPS Cyrille Artho, Armin Biere
2004	J	`jnl`	Efficient reduction of finite state model checking to reachability analysis. Int. J. Softw. Tools Technol. Transf. Viktor Schuppan, Armin Biere
2004	A*	`conf`	JNuke: Efficient Dynamic Analysis for Java. CAV Cyrille Artho, Viktor Schuppan, Armin Biere, Pascal Eugster, Marcel Baur, Boris Zweimüller
2004	—	`conf`	JVM Independent Replay in Java. RV@ETAPS Viktor Schuppan, Marcel Baur, Armin Biere
2004	—	`conf`	Preface. BMC@CAV Armin Biere, Ofer Strichman
2004	A	`conf`	Resolve and Expand. SAT Armin Biere
2004	—	`conf`	Resolve and Expand. SAT (Selected Papers Armin Biere
2004	B	`conf`	Simple Bounded LTL Model Checking. FMCAD Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila
2004	B	`conf`	Using Block-Local Atomicity to Detect Stale-Value Concurrency Errors. ATVA Cyrille Artho, Klaus Havelund, Armin Biere
2003	J	`jnl`	A satisfiability procedure for quantified Boolean formulae. Discret. Appl. Math. David A. Plaisted, Armin Biere, Yunshan Zhu
2003	J	`jnl`	Bounded model checking. Adv. Comput. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, Yunshan Zhu
2003	—	`ed.`	First International Workshop on Bounded Model Checking, BMC@CAV 2003, Boulder, Colorado, USA, July 13, 2003 BMC@CAV Ofer Strichman, Armin Biere
2003	C	`conf`	Formal Methods Group ETH Zürich. FMICS Armin Biere, Cyrille Artho, Malek Haroud, Viktor Schuppan
2003	—	`conf`	High-Level Data Races. NDDL/VVEIS Cyrille Artho, Klaus Havelund, Armin Biere
2003	J	`jnl`	High-level data races. Softw. Test. Verification Reliab. Cyrille Artho, Klaus Havelund, Armin Biere
2003	—	`conf`	Preface. BMC@CAV Ofer Strichman, Armin Biere
2003	J	`jnl`	Verifying the IEEE 1394 FireWire Tree Identify Protocol with SMV. Formal Aspects Comput. Viktor Schuppan, Armin Biere
2002	C	`conf`	Liveness Checking as Safety Checking. FMICS Armin Biere, Cyrille Artho, Viktor Schuppan
2002	A	`conf`	SAT and ATPG: Boolean engines for formal hardware verification. ICCAD Armin Biere, Wolfgang Kunz
2002	J	`jnl`	Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function. Formal Methods Syst. Des. Sergey Berezin, Edmund M. Clarke, Armin Biere, Yunshan Zhu
2001	—	`conf`	Applying Static Analysis to Large-Scale, Multi-Threaded Java Programs. Australian Software Engineering Conference Cyrille Artho, Armin Biere
2001	J	`jnl`	Bounded Model Checking Using Satisfiability Solving. Formal Methods Syst. Des. Edmund M. Clarke, Armin Biere, Richard Raimi, Yunshan Zhu
2000	A*	`conf`	Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. CAV Poul Frederick Williams, Armin Biere, Edmund M. Clarke, Anubhav Gupta
1999	—	`conf`	Combining Local and Global Model Checking. SMC@FLoC Armin Biere, Edmund M. Clarke, Yunshan Zhu
1999	—	`conf`	Multiple State and Single State Tableaux for Combining Local and Global Model Checking. Correct System Design Armin Biere, Edmund M. Clarke, Yunshan Zhu
1999	A*	`conf`	Symbolic Model Checking Using SAT Procedures instead of BDDs. DAC Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Masahiro Fujita, Yunshan Zhu
1999	A	`conf`	Symbolic Model Checking without BDDs. TACAS Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu
1999	A*	`conf`	Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs. CAV Armin Biere, Edmund M. Clarke, Richard Raimi, Yunshan Zhu
1998	B	`conf`	A Performance Study of BDD-Based Model Checking. FMCAD Bwolen Yang, Randal E. Bryant, David R. O'Hallaron, Armin Biere, Olivier Coudert, Geert Janssen, Rajeev K. Ranjan, Fabio Somenzi
1998	B	`conf`	Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification. FMCAD Sergey Berezin, Armin Biere, Edmund M. Clarke, Yunshan Zhu
1997	—	`—`	Effiziente Modellprüfung des µ-Kalküls mit binären Entscheidungsdiagrammen. Armin Biere
1997	A*	`conf`	µcke - Efficient µ-Calculus Model Checking. CAV Armin Biere