Armin Biere

Proceedings of the 26th International Conference on Theory and Applications of Satisfiability Testing, 2023

CadiBack: Extracting Backbones with CaDiCaL.

[BibT_eX]

[DOI]

Nils Froleyks

Wenxi Wang

Proceedings of the 26th International Conference on Theory and Applications of Satisfiability Testing, 2023

The SAT Museum.

[BibT_eX]

[DOI]

Proceedings of the 14th International Workshop on Pragmatics of SAT co-located with the 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), 2023

Towards Compositional Hardware Model Checking Certification.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2023

BIG Backbones.

[BibT_eX]

[DOI]

Nils Froleyks

Emily Yu

Proceedings of the Formal Methods in Computer-Aided Design, 2023

2022

Theory and Practice of SAT and Combinatorial Solving (Dagstuhl Seminar 22411).

[BibT_eX]

[DOI]

Dagstuhl Reports, October, 2022

Tools and algorithms for the construction and analysis of systems: a special issue for TACAS 2020.

[BibT_eX]

[DOI]

David Parker

Int. J. Softw. Tools Technol. Transf., 2022

Better Decision Heuristics in CDCL through Local Search and Target Phases.

[BibT_eX]

[DOI]

J. Artif. Intell. Res., 2022

Mining definitions in Kissat with Kittens.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2022

Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses.

[BibT_eX]

[DOI]

CoRR, 2022

Fuzzing and Delta Debugging And-Inverter Graph Verification Tools.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 16th International Conference, 2022

Clausal Proofs for Pseudo-Boolean Reasoning.

[BibT_eX]

[DOI]

Randal E. Bryant

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Migrating Solver State.

[BibT_eX]

[DOI]

Md. Solimul Chowdhury

Michael W. Whalen

Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing, 2022

QuAPI: Adding Assumptions to Non-Assuming SAT & QBF Solvers.

[BibT_eX]

[DOI]

Maximilian Heisinger

Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC/IJCAR 2022), Haifa, Israel, August, 11, 2022

Stratified Certification for k-Induction.

[BibT_eX]

[DOI]

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

First-Order Subsumption via SAT Solving.

[BibT_eX]

[DOI]

Jakob Rath

Laura Kovács

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification.

[BibT_eX]

[DOI]

Proceedings of the 2022 Design, Automation & Test in Europe Conference & Exhibition, 2022

2021

Preprocessing in SAT Solving.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Satisfiability - Second Edition, 2021

Bounded Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Satisfiability - Second Edition, 2021

On Enumerating Short Projected Models.

[BibT_eX]

[DOI]

Roberto Sebastiani

CoRR, 2021

SAT Solving with GPU Accelerated Inprocessing.

[BibT_eX]

[DOI]

Muhammad Osama

Anton Wijs

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

AMulet 2.0 for Verifying Multiplier Circuits.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

XOR Local Search for Boolean Brent Equations.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2021, 2021

Efficient All-UIP Learned Clause Minimization.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2021, 2021

Decomposition Strategies to Count Integer Solutions over Linear Constraints.

[BibT_eX]

[DOI]

Cunjing Ge

Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, 2021

Single Clause Assumption without Activation Literals to Speed-up IC3.

[BibT_eX]

[DOI]

Nils Froleyks

Proceedings of the Formal Methods in Computer Aided Design, 2021

Progress in Certifying Hardware Model Checking Results.

[BibT_eX]

[DOI]

Emily Yu

Keijo Heljanko

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

Non-clausal Redundancy Properties.

[BibT_eX]

[DOI]

Lee A. Barnett

Proceedings of the Automated Deduction - CADE 28, 2021

2020

Simulating Strong Practical Proof Systems with Extended Resolution.

[BibT_eX]

[DOI]

J. Autom. Reason., 2020

Strong Extension-Free Proof Systems.

[BibT_eX]

[DOI]

J. Autom. Reason., 2020

Preface to the Special Issue on Automated Reasoning Systems.

[BibT_eX]

[DOI]

Cesare Tinelli

Christoph Weidenbach

J. Autom. Reason., 2020

Incremental column-wise verification of arithmetic circuits using computer algebra.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2020

Four Flavors of Entailment.

[BibT_eX]

[DOI]

Roberto Sebastiani

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2020, 2020

Distributed Cube and Conquer with Paracooba.

[BibT_eX]

[DOI]

Maximilian Heisinger

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2020, 2020

Aiding an Introduction to Formal Reasoning Within a First-Year Logic Course for CS Majors Using a Mobile Self-Study App.

[BibT_eX]

[DOI]

Proceedings of the 2020 ACM Conference on Innovation and Technology in Computer Science Education, 2020

The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus.

[BibT_eX]

[DOI]

Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

Tutorial on World-Level Model Checking.

[BibT_eX]

[DOI]

Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

From DRUP to PAC and Back.

[BibT_eX]

[DOI]

Proceedings of the 2020 Design, Automation & Test in Europe Conference & Exhibition, 2020

Computational Logic in the First Semester of Computer Science: An Experience Report.

[BibT_eX]

[DOI]

Proceedings of the 12th International Conference on Computer Supported Education, 2020

Duplex Encoding of Staircase At-Most-One Constraints for the Antibandwidth Problem.

[BibT_eX]

[DOI]

Proceedings of the Integration of Constraint Programming, Artificial Intelligence, and Operations Research, 2020

Nullstellensatz-Proofs for Multiplier Verification.

[BibT_eX]

[DOI]

Proceedings of the Computer Algebra in Scientific Computing - 22nd International Workshop, 2020

Covered Clauses Are Not Propagation Redundant.

[BibT_eX]

[DOI]

Lee A. Barnett

David M. Cerna

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

SAT, Computer Algebra, Multipliers.

[BibT_eX]

[DOI]

Proceedings of the Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops, 2019

Encoding Redundancy for Satisfaction-Driven Clause Learning.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Backing Backtracking.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

Incremental Inprocessing in SAT Solving.

[BibT_eX]

[DOI]

Christoph Scholl

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

Clausal Proofs of Mutilated Chessboards.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 11th International Symposium, 2019

A Survey on Applications of Quantified Boolean Formulas.

[BibT_eX]

[DOI]

Proceedings of the 31st IEEE International Conference on Tools with Artificial Intelligence, 2019

Certifying Hardware Model Checking Results.

[BibT_eX]

[DOI]

Zhengqi Yu

Keijo Heljanko

Proceedings of the Formal Methods and Software Engineering, 2019

Combining Conflict-Driven Clause Learning and Chronological Backtracking for Propositional Model Counting.

[BibT_eX]

[DOI]

Proceedings of the GCAI 2019. Proceedings of the 5th Global Conference on Artificial Intelligence, 2019

A Framework for Model Checking Against CTLK Using Quantified Boolean Formulas.

[BibT_eX]

[DOI]

Emily Yu

Proceedings of the Formal Techniques for Safety-Critical Systems, 2019

Verifying Large Multipliers by Combining SAT and Computer Algebra.

[BibT_eX]

[DOI]

Proceedings of the 2019 Formal Methods in Computer Aided Design, 2019

Truth Assignments as Conditional Autarkies.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2019

2018

SAT-Based Model Checking.

[BibT_eX]

[DOI]

Daniel Kröning

Proceedings of the Handbook of Model Checking., 2018

Local Redundancy in SAT: Generalizations of Blocked Clauses.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2018

Revisiting Decision Diagrams for SAT.

[BibT_eX]

[DOI]

Tom van Dijk

Rüdiger Ehlers

CoRR, 2018

What a Difference a Variable Makes.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

A Practical Polynomial Calculus for Arithmetic Circuit Verification.

[BibT_eX]

[DOI]

Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation co-located with Federated Logic Conference, 2018

Two flavors of DRAT.

[BibT_eX]

[DOI]

Adrián Rebola-Pardo

Proceedings of Pragmatics of SAT 2015, 2018

The Effect of Scrambling CNFs.

[BibT_eX]

[DOI]

Proceedings of Pragmatics of SAT 2015, 2018

Evaluating CDCL Restart Schemes.

[BibT_eX]

[DOI]

Proceedings of Pragmatics of SAT 2015, 2018

Dualizing Projected Model Counting.

[BibT_eX]

[DOI]

Proceedings of the IEEE 30th International Conference on Tools with Artificial Intelligence, 2018

Improving and extending the algebraic approach for verifying gate-level multipliers.

[BibT_eX]

[DOI]

Proceedings of the 2018 Design, Automation & Test in Europe Conference & Exhibition, 2018

Btor2 , BtorMC and Boolector 3.0.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Fahiem Bacchus

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

Cube-and-Conquer for Satisfiability.

[BibT_eX]

[DOI]

Oliver Kullmann

Proceedings of the Handbook of Parallel Constraint Reasoning., 2018

2017

Solution Validation and Extraction for QBF Preprocessing.

[BibT_eX]

[DOI]

J. Autom. Reason., 2017

Propagation based local search for bit-precise reasoning.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2017

An Abstract Dual Propositional Model Counter.

[BibT_eX]

[DOI]

Steffen Hölldobler

Proceedings of the YSIP2, 2017

Skolem Function Continuation for Quantified Boolean Formulas.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 11th International Conference, 2017

Counterexample-Guided Model Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Challenges in Verifying Arithmetic Circuits Using Computer Algebra.

[BibT_eX]

[DOI]

Proceedings of the 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2017

Model-Based API Testing for SMT Solvers.

[BibT_eX]

[DOI]

Proceedings of the 15th International Workshop on Satisfiability Modulo Theories affiliated with the International Conference on Computer-Aided Verification (CAV 2017), Heidelberg, Germany, July 22, 2017

Blocked Clauses in First-Order Logic.

[BibT_eX]

[DOI]

Proceedings of the LPAR-21, 2017

Blockedness in Propositional Logic: Are You Satisfied With Your Neighborhood?

[BibT_eX]

[DOI]

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, 2017

PRuning Through Satisfaction.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2017

Column-wise verification of multipliers using computer algebra.

[BibT_eX]

[DOI]

Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

Hardware model checking competition 2017.

[BibT_eX]

[DOI]

Tom van Dijk

Keijo Heljanko

Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

Short Proofs Without New Variables.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 26, 2017

2016

Complexity of Fixed-Size Bit-Vector Logics.

[BibT_eX]

[DOI]

Theory Comput. Syst., 2016

SAT Race 2015.

[BibT_eX]

[DOI]

Artif. Intell., 2016

A Duality-Aware Calculus for Quantified Boolean Formulas.

[BibT_eX]

[DOI]

Proceedings of the 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2016

Greedy combinatorial test case generation using unsatisfiable cores.

[BibT_eX]

[DOI]

Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, 2016

Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

Super-Blocked Clauses.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015

Clause Elimination for SAT and QSAT.

[BibT_eX]

[DOI]

J. Artif. Intell. Res., 2015

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

[BibT_eX]

[DOI]

Dagstuhl Reports, 2015

Evaluating CDCL Variable Scoring Schemes.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2015, 2015

Blocked Literals Are Universal.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 7th International Symposium, 2015

Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Clausal Proof Compression.

[BibT_eX]

[DOI]

Proceedings of the IWIL@LPAR 2015, 2015

Compositional Propositional Proofs.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Optimization of Combinatorial Testing by Incremental SAT Solving.

[BibT_eX]

[DOI]

Proceedings of the 8th IEEE International Conference on Software Testing, 2015

Better Lemmas with Lambda Extraction.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2015

Stochastic Local Search for Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Christoph M. Wintersteiger

Youssef Hamadi

Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, 2015

2014

Améliorer SAT dans le cadre incrémental.

[BibT_eX]

[DOI]

Rev. d'Intelligence Artif., 2014

Boolector 2.0.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2014

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

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2014

Concurrent Cube-and-Conquer.

[BibT_eX]

[DOI]

Peter van der Tak

CoRR, 2014

iDQ: Instantiation-Based DQBF Solving.

[BibT_eX]

[DOI]

Proceedings of the POS-14. Fifth Pragmatics of SAT workshop, 2014

Detecting Cardinality Constraints in CNF.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

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).

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2014, 2014

Experimenting with SAT Solvers in Vampire.

[BibT_eX]

[DOI]

Proceedings of the Human-Inspired Computing and Its Applications, 2014

On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Computer Science 2014, 2014

Turbo-charging Lemmas on demand with don't care reasoning.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2014

Efficient extraction of Skolem functions from QRAT proofs.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2014

Challenges in bit-precise reasoning.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2014

A Unified Proof System for QBF Preprocessing.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

SAT solving experiments in Vampire.

[BibT_eX]

[DOI]

Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014, 2014

2013

The Auspicious Couple: Symbolic Execution and WCET Analysis.

[BibT_eX]

[DOI]

Proceedings of the 13th International Workshop on Worst-Case Execution Time Analysis, 2013

Model-Based Testing for Verification Back-Ends.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 7th International Conference, 2013

Factoring Out Assumptions to Speed Up MUS Extraction.

[BibT_eX]

[DOI]

Jean-Marie Lagniez

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2013, 2013

Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures.

[BibT_eX]

[DOI]

Proceedings of the POS-13. Fourth Pragmatics of SAT workshop, 2013

Blocked Clause Decomposition.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

Modbat: A Model-Based API Tester for Event-Driven Systems.

[BibT_eX]

[DOI]

Cyrille Valentin Artho

Proceedings of the Hardware and Software: Verification and Testing, 2013

Lemmas on Demand for Lambdas.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Alexandra Goultiaeva

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.

[BibT_eX]

[DOI]

Proceedings of the Computer Science - Theory and Applications, 2013

Revisiting Hyper Binary Resolution.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-24, 2013

SmacC: A Retargetable Symbolic Execution Engine.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2013

2012

Simulating Circuit-Level Simplifications on CNF.

[BibT_eX]

[DOI]

J. Autom. Reason., 2012

Managing SAT inconsistencies with HUMUS.

[BibT_eX]

[DOI]

Alexander Nöhrer

Alexander Egyed

Proceedings of the Sixth International Workshop on Variability Modelling of Software-Intensive Systems, 2012

A comparison of strategies for tolerating inconsistencies during decision-making.

[BibT_eX]

[DOI]

Alexander Nöhrer

Alexander Egyed

Proceedings of the 16th International Software Product Line Conference, 2012

Guided Merging of Sequence Diagrams.

[BibT_eX]

[DOI]

Proceedings of the Software Language Engineering, 5th International Conference, 2012

Concurrent Cube-and-Conquer - (Poster Presentation).

[BibT_eX]

[DOI]

Peter van der Tak

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2012, 2012

Resolution-Based Certificate Extraction for QBF - (Tool Presentation).

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2012, 2012

Automated Reencoding of Boolean Formulas.

[BibT_eX]

[DOI]

Norbert Manthey

Proceedings of the Hardware and Software: Verification and Testing, 2012

qbf2epr: A Tool for Generating EPR Formulas from QBF.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

Inprocessing Rules.

[BibT_eX]

[DOI]

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

Practical Aspects of SAT Solving.

[BibT_eX]

[DOI]

Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

2011

Preface.

[BibT_eX]

[DOI]

Karen Yorav

Formal Methods Syst. Des., 2011

Failed Literal Detection for QBF.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2011, 2011

Efficient CNF Simplification Based on Binary Implication Graphs.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2011, 2011

Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2011

Preprocessing and Inprocessing Techniques in SAT.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2011

Blocked Clause Elimination for QBF.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2010

Blocked Clause Elimination.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Integrating Dependency Schemes in Search-Based QBF Solvers.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2010

Reconstructing Solutions after Blocked Clause Elimination.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2010

Automated Testing and Debugging of SAT and QBF Solvers.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2010

Covered Clause Elimination.

[BibT_eX]

[DOI]

Proceedings of the Short papers for 17th International Conference on Logic for Programming, 2010

Clause Elimination Procedures for CNF Formulas.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

2009

Bounded Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Satisfiability, 2009

Lemmas on Demand for the Extensional Theory of Arrays.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2009

Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2009

Minimizing Learned Clauses.

[BibT_eX]

[DOI]

Niklas Sörensson

Proceedings of the Theory and Applications of Satisfiability Testing, 2009

A Compact Representation for Syntactic Dependencies in QBFs.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2009

SAT, SMT and Applications.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming and Nonmonotonic Reasoning, 2009

Effective Bit-Width and Under-Approximation.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Systems Theory, 2009

2008

PicoSAT Essentials.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2008

Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers.

[BibT_eX]

[DOI]

Proceedings of the International Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, 2008

Nenofex: Expanding NNF for QBF Solving.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2008

Adaptive Restart Strategies for Conflict Driven SAT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2008

Consistency Checking of All Different Constraints over Bit-Vectors within a SAT Solver.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2008

Tutorial on Model Checking: Modelling and Verification in Computer Science.

[BibT_eX]

[DOI]

Christoph M. Wintersteiger

Proceedings of the Algebraic Biology, Third International Conference, 2008

2007

A First Step Towards a Unified Proof Checker for QBF.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2007

Efficient Model Checking of Applications with Input/Output.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Systems Theory, 2007

C32SAT: Checking C Expressions.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006

Linear Encodings of Bounded LTL Model Checking.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2006

Decomposing SAT Problems into Connected Components.

[BibT_eX]

[DOI]

Carsten Sinz

J. Satisf. Boolean Model. Comput., 2006

Compressing BMC Encodings with QBF.

[BibT_eX]

[DOI]

Toni Jussila

Proceedings of the Fourth International Workshop on Bounded Model Checking, 2006

Extended Resolution Proofs for Symbolic SAT Solving with Quantification.

[BibT_eX]

[DOI]

Toni Jussila

Carsten Sinz

Proceedings of the Theory and Applications of Satisfiability Testing, 2006

Advanced Unit Testing: How to Scale up a Unit Test Framework.

[BibT_eX]

[DOI]

Proceedings of the 2006 International Workshop on Automation of Software Test, 2006

Exhaustive Testing of Exception Handlers with Enforcer.

[BibT_eX]

[DOI]

Shinichi Honiden

Proceedings of the Formal Methods for Components and Objects, 5th International Symposium, 2006

Enforcer - Efficient Failure Injection.

[BibT_eX]

[DOI]

Shinichi Honiden

Proceedings of the FM 2006: Formal Methods, 2006

Extended Resolution Proofs for Conjoining BDDs.

[BibT_eX]

[DOI]

Carsten Sinz

Proceedings of the Computer Science, 2006

2005

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

[BibT_eX]

[DOI]

Mukul R. Prasad

Aarti Gupta

Int. J. Softw. Tools Technol. Transf., 2005

Introductory paper.

[BibT_eX]

[DOI]

Ofer Strichman

Int. J. Softw. Tools Technol. Transf., 2005

Liveness Checking as Safety Checking for Infinite State Spaces.

[BibT_eX]

[DOI]

Proceedings of the 7th International Workshop on Verification of Infinite-State Systems, 2005

Preface.

[BibT_eX]

[DOI]

Ofer Strichman

Proceedings of the Third International Workshop on Bounded Model Checking, 2005

Subroutine Inlining and Bytecode Abstraction to Simplify Static and Dynamic Analysis.

[BibT_eX]

[DOI]

Proceedings of the First Workshop on Bytecode Semantics, 2005

Combined Static and Dynamic Analysis.

[BibT_eX]

[DOI]

Proceedings of the First International Workshop on Abstract Interpretation of Object-oriented Languages, 2005

Simple Is Better: Efficient Bounded Model Checking for Past LTL.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2005

Shortest Counterexamples for Symbolic Model Checking of LTL with Past.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

SDL Versus C Equivalence Checking.

[BibT_eX]

[DOI]

Malek Haroud

Proceedings of the SDL 2005: Model Driven, 2005

Effective Preprocessing in SAT Through Variable and Clause Elimination.

[BibT_eX]

[DOI]

Niklas Eén

Proceedings of the Theory and Applications of Satisfiability Testing, 2005

2004

Efficient reduction of finite state model checking to reachability analysis.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2004

JVM Independent Replay in Java.

[BibT_eX]

[DOI]

Marcel Baur

Proceedings of the Fourth Workshop on Runtime Verification, 2004

Resolve and Expand.

[BibT_eX]

[DOI]

Proceedings of the SAT 2004, 2004

Simple Bounded LTL Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 5th International Conference, 2004

JNuke: Efficient Dynamic Analysis for Java.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Using Block-Local Atomicity to Detect Stale-Value Concurrency Errors.

[BibT_eX]

[DOI]

Klaus Havelund

Proceedings of the Automated Technology for Verification and Analysis: Second International Conference, 2004

2003

High-level data races.

[BibT_eX]

[DOI]

Klaus Havelund

Softw. Test. Verification Reliab., 2003

Verifying the IEEE 1394 FireWire Tree Identify Protocol with SMV.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2003

Formal Methods Group ETH Zürich.

[BibT_eX]

[DOI]

Proceedings of the Eighth International Workshop on Formal Methods for Industrial Critical Systems, 2003

A satisfiability procedure for quantified Boolean formulae.

[BibT_eX]

[DOI]

David A. Plaisted

Yunshan Zhu

Discret. Appl. Math., 2003

Bounded model checking.

[BibT_eX]

[DOI]

Adv. Comput., 2003

2002

Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2002

Liveness Checking as Safety Checking.

[BibT_eX]

[DOI]

Proceedings of the 7th International ERCIM Workshop in Formal Methods for Industrial Critical Systems, 2002

SAT and ATPG: Boolean engines for formal hardware verification.

[BibT_eX]

[DOI]

Wolfgang Kunz

Proceedings of the 2002 IEEE/ACM International Conference on Computer-aided Design, 2002

2001

Bounded Model Checking Using Satisfiability Solving.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2001

Applying Static Analysis to Large-Scale, Multi-Threaded Java Programs.

[BibT_eX]

[DOI]

Proceedings of the 13th Australian Software Engineering Conference (ASWEC 2001), 2001

2000

Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking.

[BibT_eX]

[DOI]

Poul Frederick Williams

Edmund M. Clarke

Anubhav Gupta

Proceedings of the Computer Aided Verification, 12th International Conference, 2000

1999

Combining Local and Global Model Checking.

[BibT_eX]

[DOI]

Edmund M. Clarke

Yunshan Zhu

Proceedings of the First International Workshop on Symbolic Model Checking, 1999

Symbolic Model Checking without BDDs.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1999

Symbolic Model Checking Using SAT Procedures instead of BDDs.

[BibT_eX]

[DOI]

Proceedings of the 36th Conference on Design Automation, 1999

Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 11th International Conference, 1999

Multiple State and Single State Tableaux for Combining Local and Global Model Checking.

[BibT_eX]

[DOI]

Edmund M. Clarke

Yunshan Zhu

Proceedings of the Correct System Design, 1999

1998

A Performance Study of BDD-Based Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 1998

Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 1998

1997

µcke - Efficient µ-Calculus Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 9th International Conference, 1997

Effiziente Modellprüfung des µ-Kalküls mit binären Entscheidungsdiagrammen.

[BibT_eX]

[DOI]