2023
Lightweight Online Learning for Sets of Related Problems in Automated Reasoning.
Proceedings of the Formal Methods in Computer-Aided Design, 2023
G-QED: Generalized QED Pre-silicon Verification beyond Non-Interfering Hardware Accelerators.
,
,
,
,
,
,
,
,
,
,
,
Proceedings of the 60th ACM/IEEE Design Automation Conference, 2023
2021
Quantified Boolean Formulas.
Proceedings of the Handbook of Satisfiability - Second Edition, 2021
Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations.
Formal Methods Syst. Des., 2021
Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection.
CoRR, 2021
Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition.
,
,
,
,
,
,
,
,
,
,
,
,
,
,
Proceedings of the Formal Methods in Computer Aided Design, 2021
Pono: A Flexible and Extensible SMT-Based Model Checker.
Proceedings of the Computer Aided Verification - 33rd International Conference, 2021
2020
A Theoretical Framework for Symbolic Quick Error Detection.
Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020
A-QED Verification of Hardware Accelerators.
,
,
,
,
,
,
,
,
,
,
,
,
Proceedings of the 57th ACM/IEEE Design Automation Conference, 2020
2019
QBFRelay, QRATPre+, and DepQBF: Incremental Preprocessing Meets Search-Based QBF Solving.
J. Satisf. Boolean Model. Comput., 2019
QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019
Unlocking the Power of Formal Hardware Verification with CoSA and Symbolic QED: Invited Paper.
Proceedings of the International Conference on Computer-Aided Design, 2019
2018
Expansion-Based QBF Solving Without Recursion.
Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018
Evaluating QBF Solvers: Quantifier Alternations Matter.
Proceedings of the Principles and Practice of Constraint Programming, 2018
QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property.
Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018
Parallel Solving of Quantified Boolean Formulas.
Proceedings of the Handbook of Parallel Constraint Reasoning., 2018
2017
Conformant planning as a case study of incremental QBF solving.
Ann. Math. Artif. Intell., 2017
DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL.
Proceedings of the Automated Deduction - CADE 26, 2017
2016
Satisfiability-Based Methods for Reactive Synthesis from Safety Specifications.
CoRR, 2016
The QBF Gallery: Behind the scenes.
Artif. Intell., 2016
Q-Resolution with Generalized Axioms.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016
HordeQBF: A Modular and Massively Parallel QBF Solver.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016
2015
Clause Elimination for SAT and QSAT.
J. Artif. Intell. Res., 2015
Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2015, 2015
Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015
Automated Benchmarking of Incremental SAT and QBF Solvers.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015
2014
The QBFGallery 2014: The QBF Competition at the FLoC Olympic Games.
J. Satisf. Boolean Model. Comput., 2014
MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2014, 2014
Incremental QBF Solving by DepQBF.
Proceedings of the Mathematical Software - ICMS 2014, 2014
SAT-based methods for circuit synthesis.
Proceedings of the Formal Methods in Computer-Aided Design, 2014
Proceedings of the Principles and Practice of Constraint Programming, 2014
2013
Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2013, 2013
Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013
2012
Resolution-Based Certificate Extraction for QBF - (Tool Presentation).
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2012, 2012
Extended Failed-Literal Preprocessing for Quantified Boolean Formulas.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2012, 2012
qbf2epr: A Tool for Generating EPR Formulas from QBF.
Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, 2012
2011
Failed Literal Detection for QBF.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2011, 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.
J. Satisf. Boolean Model. Comput., 2010
Integrating Dependency Schemes in Search-Based QBF Solvers.
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
2009
A Compact Representation for Syntactic Dependencies in QBFs.
Proceedings of the Theory and Applications of Satisfiability Testing, 2009
2008
Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers.
Proceedings of the International Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, 2008
Nenofex: Expanding NNF for QBF Solving.
Proceedings of the Theory and Applications of Satisfiability Testing, 2008