Florian Lonsing

Publication Activity (10 Years)

Years Active: 2008-2023
Publications (10 Years): 30

Top Topics

Boolean Formula

Error Detection

Top Venues

Publications

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
G-QED: Generalized QED Pre-silicon Verification beyond Non-Interfering Hardware Accelerators. DAC (2023)
Haoze Wu, Christopher Hahn, Florian Lonsing, Makai Mann, Raghuram Ramanujan, Clark W. Barrett
Lightweight Online Learning for Sets of Related Problems in Automated Reasoning. CoRR (2023)
Haoze Wu, Christopher Hahn, Florian Lonsing, Makai Mann, Raghuram Ramanujan, Clark W. Barrett
Lightweight Online Learning for Sets of Related Problems in Automated Reasoning. FMCAD (2023)
Saranyu Chattopadhyay, Florian Lonsing, Luca Piccolboni, Deepraj Soni, Peng Wei, Xiaofan Zhang, Yuan Zhou, Luca P. Carloni, Deming Chen, Jason Cong, Ramesh Karri, Zhiru Zhang, Caroline Trippel, Clark W. Barrett, Subhasish Mitra
Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition. FMCAD (2021)
Roderick Bloem, Nicolas Braud-Santoni, Vedad Hadzic, Uwe Egly, Florian Lonsing, Martina Seidl
Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations. Formal Methods Syst. Des. 57 (2) (2021)
Karthik Ganesan, Florian Lonsing, Srinivasa Shashank Nuthakki, Eshan Singh, Mohammad Rahmani Fadiheh, Wolfgang Kunz, Dominik Stoffel, Clark W. Barrett, Subhasish Mitra
Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection. CoRR (2021)
Makai Mann, Ahmed Irfan, Florian Lonsing, Yahan Yang, Hongce Zhang, Kristopher Brown, Aarti Gupta, Clark W. Barrett
Pono: A Flexible and Extensible SMT-Based Model Checker. CAV (2) (2021)
Saranyu Chattopadhyay, Florian Lonsing, Luca Piccolboni, Deepraj Soni, Peng Wei, Xiaofan Zhang, Yuan Zhou, Luca P. Carloni, Deming Chen, Jason Cong, Ramesh Karri, Zhiru Zhang, Caroline Trippel, Clark W. Barrett, Subhasish Mitra
Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition. CoRR (2021)
Eshan Singh, Florian Lonsing, Saranyu Chattopadhyay, Maxwell Strange, Peng Wei, Xiaofan Zhang, Yuan Zhou, Deming Chen, Jason Cong, Priyanka Raina, Zhiru Zhang, Clark W. Barrett, Subhasish Mitra
A-QED Verification of Hardware Accelerators. DAC (2020)
Florian Lonsing, Subhasish Mitra, Clark W. Barrett
A Theoretical Framework for Symbolic Quick Error Detection. CoRR (2020)
Florian Lonsing, Subhasish Mitra, Clark W. Barrett
A Theoretical Framework for Symbolic Quick Error Detection. FMCAD (2020)
Florian Lonsing, Uwe Egly
QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties. CoRR (2019)
Florian Lonsing, Karthik Ganesan, Makai Mann, Srinivasa Shashank Nuthakki, Eshan Singh, Mario Srouji, Yahan Yang, Subhasish Mitra, Clark W. Barrett
Unlocking the Power of Formal Hardware Verification with CoSA and Symbolic QED: Invited Paper. ICCAD (2019)
Florian Lonsing
QBFRelay, QRATPre+, and DepQBF: Incremental Preprocessing Meets Search-Based QBF Solving. J. Satisf. Boolean Model. Comput. 11 (1) (2019)
Florian Lonsing, Uwe Egly
QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties. SAT (2019)
Florian Lonsing, Uwe Egly
QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property. CoRR (2018)
Florian Lonsing, Uwe Egly
Evaluating QBF Solvers: Quantifier Alternations Matter. CP (2018)
Roderick Bloem, Nicolas Braud-Santoni, Vedad Hadzic, Uwe Egly, Florian Lonsing, Martina Seidl
Expansion-Based QBF Solving Without Recursion. FMCAD (2018)
Florian Lonsing, Uwe Egly
QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property. IJCAR (2018)
Roderick Bloem, Nicolas Braud-Santoni, Vedad Hadzic, Uwe Egly, Florian Lonsing, Martina Seidl
Expansion-Based QBF Solving Without Recursion. CoRR (2018)
Florian Lonsing, Uwe Egly
DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL. CoRR (2017)
Uwe Egly, Martin Kronegger, Florian Lonsing, Andreas Pfandler
Conformant planning as a case study of incremental QBF solving. Ann. Math. Artif. Intell. 80 (1) (2017)
Florian Lonsing, Uwe Egly
DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL. CADE (2017)
Florian Lonsing, Uwe Egly
Evaluating QBF Solvers: Quantifier Alternations Matter. CoRR (2017)
Tomás Balyo, Florian Lonsing
HordeQBF: A Modular and Massively Parallel QBF Solver. CoRR (2016)
Florian Lonsing, Martina Seidl, Allen Van Gelder
The QBF Gallery: Behind the scenes. Artif. Intell. 237 (2016)
Roderick Bloem, Uwe Egly, Patrick Klampfl, Robert Könighofer, Florian Lonsing, Martina Seidl
Satisfiability-Based Methods for Reactive Synthesis from Safety Specifications. CoRR (2016)
Florian Lonsing, Uwe Egly, Martina Seidl
Q-Resolution with Generalized Axioms. SAT (2016)
Florian Lonsing, Uwe Egly, Martina Seidl
Q-Resolution with Generalized Axioms. CoRR (2016)
Tomás Balyo, Florian Lonsing
HordeQBF: A Modular and Massively Parallel QBF Solver. SAT (2016)
Florian Lonsing, Fahiem Bacchus, Armin Biere, Uwe Egly, Martina Seidl
Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination. LPAR (2015)
Florian Lonsing, Martina Seidl, Allen Van Gelder
The QBF Gallery: Behind the Scenes. CoRR (2015)
Uwe Egly, Florian Lonsing, Johannes Oetsch
Automated Benchmarking of Incremental SAT and QBF Solvers. LPAR (2015)
Florian Lonsing, Uwe Egly
Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API. SAT (2015)
Florian Lonsing, Uwe Egly
Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API. CoRR (2015)
Marijn Heule, Matti Järvisalo, Florian Lonsing, Martina Seidl, Armin Biere
Clause Elimination for SAT and QSAT. J. Artif. Intell. Res. 53 (2015)
Uwe Egly, Florian Lonsing, Johannes Oetsch
Automated Benchmarking of Incremental SAT and QBF Solvers. CoRR (2015)
Florian Lonsing, Uwe Egly
Incremental QBF Solving. CP (2014)
Charles Jordan, Lukasz Kaiser, Florian Lonsing, Martina Seidl
MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing. SAT (2014)
Uwe Egly, Martin Kronegger, Florian Lonsing, Andreas Pfandler
Conformant Planning as a Case Study of Incremental QBF Solving. CoRR (2014)
Florian Lonsing, Uwe Egly
Incremental QBF Solving by DepQBF. ICMS (2014)
Uwe Egly, Martin Kronegger, Florian Lonsing, Andreas Pfandler
Conformant Planning as a Case Study of Incremental QBF Solving. AISC (2014)
Roderick Bloem, Uwe Egly, Patrick Klampfl, Robert Könighofer, Florian Lonsing
SAT-Based Methods for Circuit Synthesis. CoRR (2014)
Roderick Bloem, Uwe Egly, Patrick Klampfl, Robert Könighofer, Florian Lonsing
SAT-based methods for circuit synthesis. FMCAD (2014)
Mikolas Janota, Charles Jordan, Will Klieber, Florian Lonsing, Martina Seidl, Allen Van Gelder
The QBFGallery 2014: The QBF Competition at the FLoC Olympic Games. J. Satisf. Boolean Model. Comput. 9 (1) (2014)
Florian Lonsing, Uwe Egly
Incremental QBF Solving. CoRR (2014)
Uwe Egly, Florian Lonsing, Magdalena Widl
Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving. LPAR (2013)
Florian Lonsing, Uwe Egly, Allen Van Gelder
Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation. SAT (2013)
Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, Armin Biere
Resolution-Based Certificate Extraction for QBF - (Tool Presentation). SAT (2012)
Allen Van Gelder, Samuel B. Wood, Florian Lonsing
Extended Failed-Literal Preprocessing for Quantified Boolean Formulas. SAT (2012)
Martina Seidl, Florian Lonsing, Armin Biere
qbf2epr: A Tool for Generating EPR Formulas from QBF. PAAR@IJCAR (2012)
Armin Biere, Florian Lonsing, Martina Seidl
Blocked Clause Elimination for QBF. CADE (2011)
Florian Lonsing, Armin Biere
Failed Literal Detection for QBF. SAT (2011)
Florian Lonsing, Armin Biere
DepQBF: A Dependency-Aware QBF Solver. J. Satisf. Boolean Model. Comput. 7 (2-3) (2010)
Florian Lonsing, Armin Biere
Integrating Dependency Schemes in Search-Based QBF Solvers. SAT (2010)
Robert Brummayer, Florian Lonsing, Armin Biere
Automated Testing and Debugging of SAT and QBF Solvers. SAT (2010)
Florian Lonsing, Armin Biere
Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers. Electron. Notes Theor. Comput. Sci. 251 (2009)
Florian Lonsing, Armin Biere
A Compact Representation for Syntactic Dependencies in QBFs. SAT (2009)
Florian Lonsing, Armin Biere
Nenofex: Expanding NNF for QBF Solving. SAT (2008)