Florian Lonsing

According to our database, Florian Lonsing authored at least 44 papers between 2008 and 2023.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2023

Lightweight Online Learning for Sets of Related Problems in Automated Reasoning.

Haoze Wu, Christopher Hahn, Florian Lonsing, Makai Mann, Raghuram Ramanujan, Clark W. Barrett

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

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

Proceedings of the 60th ACM/IEEE Design Automation Conference, 2023

2021

Quantified Boolean Formulas.

Olaf Beyersdorff, Mikolás Janota, Florian Lonsing, Martina Seidl

Proceedings of the Handbook of Satisfiability - Second Edition, 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

Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection.

Karthik Ganesan, Florian Lonsing, Srinivasa Shashank Nuthakki, Eshan Singh, Mohammad Rahmani Fadiheh, Wolfgang Kunz, Dominik Stoffel, Clark W. Barrett, Subhasish Mitra

CoRR, 2021

Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition.

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

Proceedings of the Formal Methods in Computer Aided Design, 2021

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

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

2020

A Theoretical Framework for Symbolic Quick Error Detection.

Florian Lonsing, Subhasish Mitra, Clark W. Barrett

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

A-QED Verification of Hardware Accelerators.

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

Proceedings of the 57th ACM/IEEE Design Automation Conference, 2020

2019

QBFRelay, QRATPre+, and DepQBF: Incremental Preprocessing Meets Search-Based QBF Solving.

Florian Lonsing

J. Satisf. Boolean Model. Comput., 2019

QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties.

Florian Lonsing, Uwe Egly

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.

Florian Lonsing, Karthik Ganesan, Makai Mann, Srinivasa Shashank Nuthakki, Eshan Singh, Mario Srouji, Yahan Yang, Subhasish Mitra, Clark W. Barrett

Proceedings of the International Conference on Computer-Aided Design, 2019

2018

Expansion-Based QBF Solving Without Recursion.

Roderick Bloem, Nicolas Braud-Santoni, Vedad Hadzic, Uwe Egly, Florian Lonsing, Martina Seidl

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

Evaluating QBF Solvers: Quantifier Alternations Matter.

Florian Lonsing, Uwe Egly

Proceedings of the Principles and Practice of Constraint Programming, 2018

QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property.

Florian Lonsing, Uwe Egly

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

Parallel Solving of Quantified Boolean Formulas.

Florian Lonsing, Martina Seidl

Proceedings of the Handbook of Parallel Constraint Reasoning., 2018

2017

Conformant planning as a case study of incremental QBF solving.

Uwe Egly, Martin Kronegger, Florian Lonsing, Andreas Pfandler

Ann. Math. Artif. Intell., 2017

DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL.

Florian Lonsing, Uwe Egly

Proceedings of the Automated Deduction - CADE 26, 2017

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

The QBF Gallery: Behind the scenes.

Florian Lonsing, Martina Seidl, Allen Van Gelder

Artif. Intell., 2016

Q-Resolution with Generalized Axioms.

Florian Lonsing, Uwe Egly, Martina Seidl

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

HordeQBF: A Modular and Massively Parallel QBF Solver.

Tomás Balyo, Florian Lonsing

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

2015

Clause Elimination for SAT and QSAT.

Marijn Heule, Matti Järvisalo, Florian Lonsing, Martina Seidl, Armin Biere

J. Artif. Intell. Res., 2015

Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API.

Florian Lonsing, Uwe Egly

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

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

Florian Lonsing, Fahiem Bacchus, Armin Biere, Uwe Egly, Martina Seidl

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

Automated Benchmarking of Incremental SAT and QBF Solvers.

Uwe Egly, Florian Lonsing, Johannes Oetsch

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

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

MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing.

Charles Jordan, Lukasz Kaiser, Florian Lonsing, Martina Seidl

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

Incremental QBF Solving by DepQBF.

Florian Lonsing, Uwe Egly

Proceedings of the Mathematical Software - ICMS 2014, 2014

SAT-based methods for circuit synthesis.

Roderick Bloem, Uwe Egly, Patrick Klampfl, Robert Könighofer, Florian Lonsing

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

Incremental QBF Solving.

Florian Lonsing, Uwe Egly

Proceedings of the Principles and Practice of Constraint Programming, 2014

2013

Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation.

Florian Lonsing, Uwe Egly, Allen Van Gelder

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.

Uwe Egly, Florian Lonsing, Magdalena Widl

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

2012

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

Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, Armin Biere

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

Extended Failed-Literal Preprocessing for Quantified Boolean Formulas.

Allen Van Gelder, Samuel B. Wood, Florian Lonsing

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

qbf2epr: A Tool for Generating EPR Formulas from QBF.

Martina Seidl, Florian Lonsing, Armin Biere

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

2011

Failed Literal Detection for QBF.

Florian Lonsing, Armin Biere

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

Blocked Clause Elimination for QBF.

Armin Biere, Florian Lonsing, Martina Seidl

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.

Florian Lonsing, Armin Biere

J. Satisf. Boolean Model. Comput., 2010

Integrating Dependency Schemes in Search-Based QBF Solvers.

Florian Lonsing, Armin Biere

Proceedings of the Theory and Applications of Satisfiability Testing, 2010

Automated Testing and Debugging of SAT and QBF Solvers.

Robert Brummayer, Florian Lonsing, Armin Biere

Proceedings of the Theory and Applications of Satisfiability Testing, 2010

2009

A Compact Representation for Syntactic Dependencies in QBFs.

Florian Lonsing, Armin Biere

Proceedings of the Theory and Applications of Satisfiability Testing, 2009

2008

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

Florian Lonsing, Armin Biere

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

Nenofex: Expanding NNF for QBF Solving.

Florian Lonsing, Armin Biere

Proceedings of the Theory and Applications of Satisfiability Testing, 2008