Armin Biere

According to our database1, Armin Biere authored at least 152 papers between 1997 and 2018.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2018
SAT-Based Model Checking.
Proceedings of the Handbook of Model Checking., 2018

Local Redundancy in SAT: Generalizations of Blocked Clauses.
Logical Methods in Computer Science, 2018

What a Difference a Variable Makes.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Dualizing Projected Model Counting.
Proceedings of the IEEE 30th International Conference on Tools with Artificial Intelligence, 2018

Improving and extending the algebraic approach for verifying gate-level multipliers.
Proceedings of the 2018 Design, Automation & Test in Europe Conference & Exhibition, 2018

Btor2 , BtorMC and Boolector 3.0.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories.
Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

Cube-and-Conquer for Satisfiability.
Proceedings of the Handbook of Parallel Constraint Reasoning., 2018

2017
Solution Validation and Extraction for QBF Preprocessing.
J. Autom. Reasoning, 2017

Propagation based local search for bit-precise reasoning.
Formal Methods in System Design, 2017

An Abstract Dual Propositional Model Counter.
Proceedings of the YSIP2, 2017

Skolem Function Continuation for Quantified Boolean Formulas.
Proceedings of the Tests and Proofs - 11th International Conference, 2017

Counterexample-Guided Model Synthesis.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Challenges in Verifying Arithmetic Circuits Using Computer Algebra.
Proceedings of the 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2017

Blocked Clauses in First-Order Logic.
Proceedings of the LPAR-21, 2017

Blockedness in Propositional Logic: Are You Satisfied With Your Neighborhood?
Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, 2017

PRuning Through Satisfaction.
Proceedings of the Hardware and Software: Verification and Testing, 2017

Column-wise verification of multipliers using computer algebra.
Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

Hardware model checking competition 2017.
Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

Short Proofs Without New Variables.
Proceedings of the Automated Deduction - CADE 26, 2017

2016
Complexity of Fixed-Size Bit-Vector Logics.
Theory Comput. Syst., 2016

SAT Race 2015.
Artif. Intell., 2016

A Duality-Aware Calculus for Quantified Boolean Formulas.
Proceedings of the 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2016

Greedy combinatorial test case generation using unsatisfiable cores.
Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, 2016

Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

Super-Blocked Clauses.
Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015
Clause Elimination for SAT and QSAT.
J. Artif. Intell. Res., 2015

Theory and Practice of SAT Solving (Dagstuhl Seminar 15171).
Dagstuhl Reports, 2015

Evaluating CDCL Variable Scoring Schemes.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2015, 2015

Blocked Literals Are Universal.
Proceedings of the NASA Formal Methods - 7th International Symposium, 2015

Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Clausal Proof Compression.
Proceedings of the IWIL@LPAR 2015, 2015

Compositional Propositional Proofs.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Optimization of Combinatorial Testing by Incremental SAT Solving.
Proceedings of the 8th IEEE International Conference on Software Testing, 2015

Better Lemmas with Lambda Extraction.
Proceedings of the Formal Methods in Computer-Aided Design, 2015

Stochastic Local Search for Satisfiability Modulo Theories.
Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, 2015

2014
Améliorer SAT dans le cadre incrémental.
Revue d'Intelligence Artificielle, 2014

Boolector 2.0.
JSAT, 2014

Hardware Model Checking Competition 2014: An Analysis and Comparison of Solvers and Benchmarks.
JSAT, 2014

iDQ: Instantiation-Based DQBF Solving.
Proceedings of the POS-14. Fifth Pragmatics of SAT workshop, 2014

Detecting Cardinality Constraints in CNF.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2014, 2014

Lingeling Essentials, A Tutorial on Design and Implementation Aspects of the the SAT Solver Lingeling.
Proceedings of the POS-14. Fifth Pragmatics of SAT workshop, 2014

Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask).
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2014, 2014

Improving Implementation of SLS Solvers for SAT and New Heuristics for k-SAT with Long Clauses.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2014, 2014

Experimenting with SAT Solvers in Vampire.
Proceedings of the Human-Inspired Computing and Its Applications, 2014

On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic.
Proceedings of the Mathematical Foundations of Computer Science 2014, 2014

Turbo-charging Lemmas on demand with don't care reasoning.
Proceedings of the Formal Methods in Computer-Aided Design, 2014

Efficient extraction of Skolem functions from QRAT proofs.
Proceedings of the Formal Methods in Computer-Aided Design, 2014

Challenges in bit-precise reasoning.
Proceedings of the Formal Methods in Computer-Aided Design, 2014

A Unified Proof System for QBF Preprocessing.
Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

SAT solving experiments in Vampire.
Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014, 2014

2013
The Auspicious Couple: Symbolic Execution and WCET Analysis.
Proceedings of the 13th International Workshop on Worst-Case Execution Time Analysis, 2013

Model-Based Testing for Verification Back-Ends.
Proceedings of the Tests and Proofs - 7th International Conference, 2013

Factoring Out Assumptions to Speed Up MUS Extraction.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2013, 2013

Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures.
Proceedings of the POS-13. Fourth Pragmatics of SAT workshop, 2013

Blocked Clause Decomposition.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

Modbat: A Model-Based API Tester for Event-Driven Systems.
Proceedings of the Hardware and Software: Verification and Testing, 2013

Lemmas on Demand for Lambdas.
Proceedings of the Second International Workshop on Design and Implementation of Formal Tools and Systems, 2013

Bridging the gap between dual propagation and CNF-based QBF solving.
Proceedings of the Design, Automation and Test in Europe, 2013

More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics with Binary Encoding.
Proceedings of the Computer Science - Theory and Applications, 2013

Revisiting Hyper Binary Resolution.
Proceedings of the Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, 2013

: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into.
Proceedings of the Automated Deduction - CADE-24, 2013

SmacC: A Retargetable Symbolic Execution Engine.
Proceedings of the Automated Technology for Verification and Analysis, 2013

2012
Simulating Circuit-Level Simplifications on CNF.
J. Autom. Reasoning, 2012

Managing SAT inconsistencies with HUMUS.
Proceedings of the Sixth International Workshop on Variability Modelling of Software-Intensive Systems, 2012

A comparison of strategies for tolerating inconsistencies during decision-making.
Proceedings of the 16th International Software Product Line Conference, 2012

Guided Merging of Sequence Diagrams.
Proceedings of the Software Language Engineering, 5th International Conference, 2012

Concurrent Cube-and-Conquer - (Poster Presentation).
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2012, 2012

Resolution-Based Certificate Extraction for QBF - (Tool Presentation).
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2012, 2012

Automated Reencoding of Boolean Formulas.
Proceedings of the Hardware and Software: Verification and Testing, 2012

qbf2epr: A Tool for Generating EPR Formulas from QBF.
Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, 2012

On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width.
Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

Inprocessing Rules.
Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

Practical Aspects of SAT Solving.
Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, 2012

Practical Aspects of SAT Solving.
Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

2011
Preface.
Formal Methods in System Design, 2011

Failed Literal Detection for QBF.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2011, 2011

Efficient CNF Simplification Based on Binary Implication Graphs.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2011, 2011

Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads.
Proceedings of the Hardware and Software: Verification and Testing, 2011

Preprocessing and Inprocessing Techniques in SAT.
Proceedings of the Hardware and Software: Verification and Testing, 2011

Blocked Clause Elimination for QBF.
Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010
DepQBF: A Dependency-Aware QBF Solver.
JSAT, 2010

Blocked Clause Elimination.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Integrating Dependency Schemes in Search-Based QBF Solvers.
Proceedings of the Theory and Applications of Satisfiability Testing, 2010

Reconstructing Solutions after Blocked Clause Elimination.
Proceedings of the Theory and Applications of Satisfiability Testing, 2010

Automated Testing and Debugging of SAT and QBF Solvers.
Proceedings of the Theory and Applications of Satisfiability Testing, 2010

Covered Clause Elimination.
Proceedings of the Short papers for 17th International Conference on Logic for Programming, 2010

Clause Elimination Procedures for CNF Formulas.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

2009
Bounded Model Checking.
Proceedings of the Handbook of Satisfiability, 2009

Lemmas on Demand for the Extensional Theory of Arrays.
JSAT, 2009

Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers.
Electr. Notes Theor. Comput. Sci., 2009

Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2009

Minimizing Learned Clauses.
Proceedings of the Theory and Applications of Satisfiability Testing, 2009

A Compact Representation for Syntactic Dependencies in QBFs.
Proceedings of the Theory and Applications of Satisfiability Testing, 2009

SAT, SMT and Applications.
Proceedings of the Logic Programming and Nonmonotonic Reasoning, 2009

Effective Bit-Width and Under-Approximation.
Proceedings of the Computer Aided Systems Theory, 2009

2008
PicoSAT Essentials.
JSAT, 2008

Nenofex: Expanding NNF for QBF Solving.
Proceedings of the Theory and Applications of Satisfiability Testing, 2008

Adaptive Restart Strategies for Conflict Driven SAT Solvers.
Proceedings of the Theory and Applications of Satisfiability Testing, 2008

Consistency Checking of All Different Constraints over Bit-Vectors within a SAT Solver.
Proceedings of the Formal Methods in Computer-Aided Design, 2008

Tutorial on Model Checking: Modelling and Verification in Computer Science.
Proceedings of the Algebraic Biology, Third International Conference, 2008

2007
Preface.
Electr. Notes Theor. Comput. Sci., 2007

Compressing BMC Encodings with QBF.
Electr. Notes Theor. Comput. Sci., 2007

A First Step Towards a Unified Proof Checker for QBF.
Proceedings of the Theory and Applications of Satisfiability Testing, 2007

Efficient Model Checking of Applications with Input/Output.
Proceedings of the Computer Aided Systems Theory, 2007

C32SAT: Checking C Expressions.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006
Linear Encodings of Bounded LTL Model Checking.
Logical Methods in Computer Science, 2006

Decomposing SAT Problems into Connected Components.
JSAT, 2006

Liveness Checking as Safety Checking for Infinite State Spaces.
Electr. Notes Theor. Comput. Sci., 2006

Preface.
Electr. Notes Theor. Comput. Sci., 2006

Extended Resolution Proofs for Symbolic SAT Solving with Quantification.
Proceedings of the Theory and Applications of Satisfiability Testing, 2006

Advanced Unit Testing: How to Scale up a Unit Test Framework.
Proceedings of the 2006 International Workshop on Automation of Software Test, 2006

Exhaustive Testing of Exception Handlers with Enforcer.
Proceedings of the Formal Methods for Components and Objects, 5th International Symposium, 2006

Enforcer - Efficient Failure Injection.
Proceedings of the FM 2006: Formal Methods, 2006

Extended Resolution Proofs for Conjoining BDDs.
Proceedings of the Computer Science, 2006

2005
A survey of recent advances in SAT-based formal verification.
STTT, 2005

Introductory paper.
STTT, 2005

JVM Independent Replay in Java.
Electr. Notes Theor. Comput. Sci., 2005

Preface.
Electr. Notes Theor. Comput. Sci., 2005

Subroutine Inlining and Bytecode Abstraction to Simplify Static and Dynamic Analysis.
Electr. Notes Theor. Comput. Sci., 2005

Combined Static and Dynamic Analysis.
Electr. Notes Theor. Comput. Sci., 2005

Simple Is Better: Efficient Bounded Model Checking for Past LTL.
Proceedings of the Verification, 2005

Shortest Counterexamples for Symbolic Model Checking of LTL with Past.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

SDL Versus C Equivalence Checking.
Proceedings of the SDL 2005: Model Driven, 2005

Effective Preprocessing in SAT Through Variable and Clause Elimination.
Proceedings of the Theory and Applications of Satisfiability Testing, 2005

2004
Efficient reduction of finite state model checking to reachability analysis.
STTT, 2004

Resolve and Expand.
Proceedings of the Theory and Applications of Satisfiability Testing, 2004

Resolve and Expand.
Proceedings of the SAT 2004, 2004

Simple Bounded LTL Model Checking.
Proceedings of the Formal Methods in Computer-Aided Design, 5th International Conference, 2004

JNuke: Efficient Dynamic Analysis for Java.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Using Block-Local Atomicity to Detect Stale-Value Concurrency Errors.
Proceedings of the Automated Technology for Verification and Analysis: Second International Conference, 2004

2003
Verifying the IEEE 1394 FireWire Tree Identify Protocol with SMV.
Formal Asp. Comput., 2003

Preface.
Electr. Notes Theor. Comput. Sci., 2003

Formal Methods Group ETH Zürich.
Electr. Notes Theor. Comput. Sci., 2003

A satisfiability procedure for quantified Boolean formulae.
Discrete Applied Mathematics, 2003

Bounded model checking.
Advances in Computers, 2003

High-Level Data Races.
Proceedings of the New Technologies for Information Systems, 2003

2002
Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function.
Formal Methods in System Design, 2002

Liveness Checking as Safety Checking.
Electr. Notes Theor. Comput. Sci., 2002

SAT and ATPG: Boolean engines for formal hardware verification.
Proceedings of the 2002 IEEE/ACM International Conference on Computer-aided Design, 2002

2001
Bounded Model Checking Using Satisfiability Solving.
Formal Methods in System Design, 2001

Applying Static Analysis to Large-Scale, Multi-Threaded Java Programs.
Proceedings of the 13th Australian Software Engineering Conference (ASWEC 2001), 2001

2000
Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000

1999
Combining Local and Global Model Checking.
Electr. Notes Theor. Comput. Sci., 1999

Symbolic Model Checking without BDDs.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1999

Symbolic Model Checking Using SAT Procedures instead of BDDs.
Proceedings of the 36th Conference on Design Automation, 1999

Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999

Multiple State and Single State Tableaux for Combining Local and Global Model Checking.
Proceedings of the Correct System Design, 1999

1998
A Performance Study of BDD-Based Model Checking.
Proceedings of the Formal Methods in Computer-Aided Design, 1998

Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification.
Proceedings of the Formal Methods in Computer-Aided Design, 1998

1997
µcke - Efficient µ-Calculus Model Checking.
Proceedings of the Computer Aided Verification, 9th International Conference, 1997

Effiziente Modellprüfung des µ-Kalküls mit binären Entscheidungsdiagrammen.
PhD thesis, 1997


  Loading...