Nenofex: Expanding NNF for QBF Solving. - Florian Lonsing; Armin Biere (SAT, 2008)

Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers. - Florian Lonsing; Armin Biere (MEMICS, 2008)

A Compact Representation for Syntactic Dependencies in QBFs. - Florian Lonsing; Armin Biere (SAT, 2009)

Automated Testing and Debugging of SAT and QBF Solvers. - Robert Brummayer; Florian Lonsing; Armin Biere (SAT, 2010)

Integrating Dependency Schemes in Search-Based QBF Solvers. - Florian Lonsing; Armin Biere (SAT, 2010)

DepQBF: A Dependency-Aware QBF Solver. - Florian Lonsing; Armin Biere (J. Satisf. Boolean Model. Comput., 2010)

Blocked Clause Elimination for QBF. - Armin Biere; Florian Lonsing; Martina Seidl (CADE, 2011)

Failed Literal Detection for QBF. - Florian Lonsing; Armin Biere (SAT, 2011)

qbf2epr: A Tool for Generating EPR Formulas from QBF. - Martina Seidl; Florian Lonsing; Armin Biere (PAAR@IJCAR, 2012)

Extended Failed-Literal Preprocessing for Quantified Boolean Formulas. - Allen Van Gelder; Samuel B. Wood; Florian Lonsing (SAT, 2012)

Resolution-Based Certificate Extraction for QBF - (Tool Presentation). - Aina Niemetz; Mathias Preiner; Florian Lonsing; Martina Seidl; Armin Biere (SAT, 2012)

Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving. - Uwe Egly; Florian Lonsing; Magdalena Widl (LPAR, 2013)

Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation. - Florian Lonsing; Uwe Egly; Allen Van Gelder (SAT, 2013)

Incremental QBF Solving. - Florian Lonsing; Uwe Egly (CP, 2014)

SAT-based methods for circuit synthesis. - Roderick Bloem; Uwe Egly; Patrick Klampfl; Robert Könighofer; Florian Lonsing (FMCAD, 2014)

Incremental QBF Solving by DepQBF. - Florian Lonsing; Uwe Egly (ICMS, 2014)

MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing. - Charles Jordan; Lukasz Kaiser; Florian Lonsing; Martina Seidl (SAT, 2014)

The QBFGallery 2014: The QBF Competition at the FLoC Olympic Games. - Mikolas Janota; Charles Jordan; Will Klieber; Florian Lonsing; Martina Seidl; Allen Van Gelder (J. Satisf. Boolean Model. Comput., 2014)

Automated Benchmarking of Incremental SAT and QBF Solvers. - Uwe Egly; Florian Lonsing; Johannes Oetsch (LPAR, 2015)

Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination. - Florian Lonsing; Fahiem Bacchus; Armin Biere; Uwe Egly; Martina Seidl (LPAR, 2015)

Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API. - Florian Lonsing; Uwe Egly (SAT, 2015)

Clause Elimination for SAT and QSAT. - Marijn Heule; Matti Järvisalo; Florian Lonsing; Martina Seidl; Armin Biere (J. Artif. Intell. Res., 2015)

HordeQBF: A Modular and Massively Parallel QBF Solver. - Tomás Balyo; Florian Lonsing (SAT, 2016)

Q-Resolution with Generalized Axioms. - Florian Lonsing; Uwe Egly; Martina Seidl (SAT, 2016)

The QBF Gallery: Behind the scenes. - Florian Lonsing; Martina Seidl; Allen Van Gelder (Artif. Intell., 2016)

Satisfiability-Based Methods for Reactive Synthesis from Safety Specifications. - Roderick Bloem; Uwe Egly; Patrick Klampfl; Robert Könighofer; Florian Lonsing; Martina Seidl (CoRR, 2016)

DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL. - Florian Lonsing; Uwe Egly (CADE, 2017)

Conformant planning as a case study of incremental QBF solving. - Uwe Egly; Martin Kronegger; Florian Lonsing; Andreas Pfandler (Ann. Math. Artif. Intell., 2017)

Parallel Solving of Quantified Boolean Formulas. - Florian Lonsing; Martina Seidl (Handbook of Parallel Constraint Reasoning, 2018)

QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property. - Florian Lonsing; Uwe Egly (IJCAR, 2018)

Evaluating QBF Solvers: Quantifier Alternations Matter. - Florian Lonsing; Uwe Egly (CP, 2018)

Expansion-Based QBF Solving Without Recursion. - Roderick Bloem; Nicolas Braud-Santoni; Vedad Hadzic; Uwe Egly; Florian Lonsing; Martina Seidl (FMCAD, 2018)

Unlocking the Power of Formal Hardware Verification with CoSA and Symbolic QED: Invited Paper. - Florian Lonsing; Karthik Ganesan 001; Makai Mann; Srinivasa Shashank Nuthakki; Eshan Singh; Mario Srouji; Yahan Yang; Subhasish Mitra; Clark W. Barrett (ICCAD, 2019)

QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties. - Florian Lonsing; Uwe Egly (SAT, 2019)

QBFRelay, QRATPre+, and DepQBF: Incremental Preprocessing Meets Search-Based QBF Solving. - Florian Lonsing (J. Satisf. Boolean Model. Comput., 2019)

A-QED Verification of Hardware Accelerators. - Eshan Singh; Florian Lonsing; Saranyu Chattopadhyay; Maxwell Strange; Peng Wei 004; Xiaofan Zhang 001; Yuan Zhou; Deming Chen; Jason Cong; Priyanka Raina; Zhiru Zhang; Clark W. Barrett; et al. (DAC, 2020)

A Theoretical Framework for Symbolic Quick Error Detection. - Florian Lonsing; Subhasish Mitra; Clark W. Barrett (FMCAD, 2020)

Pono: A Flexible and Extensible SMT-Based Model Checker. - Makai Mann; Ahmed Irfan; Florian Lonsing; Yahan Yang; Hongce Zhang; Kristopher Brown; Aarti Gupta; Clark W. Barrett (CAV (2), 2021)

Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition. - Saranyu Chattopadhyay; Florian Lonsing; Luca Piccolboni; Deepraj Soni; Peng Wei 004; Xiaofan Zhang 001; Yuan Zhou; Luca P. Carloni; Deming Chen; Jason Cong; Ramesh Karri; Zhiru Zhang; et al. (FMCAD, 2021)

Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection. - Karthik Ganesan 001; Florian Lonsing; Srinivasa Shashank Nuthakki; Eshan Singh; Mohammad Rahmani Fadiheh; Wolfgang Kunz; Dominik Stoffel; Clark W. Barrett; Subhasish Mitra (CoRR, 2021)

Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations. - Roderick Bloem; Nicolas Braud-Santoni; Vedad Hadzic; Uwe Egly; Florian Lonsing; Martina Seidl (Formal Methods Syst. Des., 2021)

Quantified Boolean Formulas. - Olaf Beyersdorff; Mikolás Janota; Florian Lonsing; Martina Seidl (Handbook of Satisfiability, 2021)

G-QED: Generalized QED Pre-silicon Verification beyond Non-Interfering Hardware Accelerators. - Saranyu Chattopadhyay; Keerthikumara Devarajegowda; Bihan Zhao; Florian Lonsing; Brandon A. D'Agostino; Ioanna Vavelidou; Vijay Deep Bhatt; Sebastian Prebeck; Wolfgang Ecker; Caroline Trippel; Clark W. Barrett; Subhasish Mitra (DAC, 2023)

Lightweight Online Learning for Sets of Related Problems in Automated Reasoning. - Haoze Wu 001; Christopher Hahn; Florian Lonsing; Makai Mann; Raghuram Ramanujan; Clark W. Barrett (FMCAD, 2023)