Florian Lonsing
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
33
Venues
10
Active years
2008–2026
Best venue rank
A*
Where they publish
Papers
33 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | FM | Pono 2.0: A Versatile SMT-Based Model Checker for Safety and Liveness (Long Tool Paper). | Aron Ricardo Perez-Lopez, Po-Chun Chien, Florian Lonsing, Samantha Archer, Ahmed Irfan, Clark W. Barrett |
| 2023 | DAC | 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 |
| 2023 | FMCAD | Lightweight Online Learning for Sets of Related Problems in Automated Reasoning. | Haoze Wu, Christopher Hahn, Florian Lonsing, Makai Mann, Raghuram Ramanujan, Clark W. Barrett |
| 2021 | CAV | 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 |
| 2021 | FMCAD | 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 |
| 2020 | DAC | 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 |
| 2020 | FMCAD | A Theoretical Framework for Symbolic Quick Error Detection. | Florian Lonsing, Subhasish Mitra, Clark W. Barrett |
| 2019 | ICCAD | 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 |
| 2019 | SAT | QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties. | Florian Lonsing, Uwe Egly |
| 2018 | CADE | QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property. | Florian Lonsing, Uwe Egly |
| 2018 | CP | Evaluating QBF Solvers: Quantifier Alternations Matter. | Florian Lonsing, Uwe Egly |
| 2018 | FMCAD | Expansion-Based QBF Solving Without Recursion. | Roderick Bloem, Nicolas Braud-Santoni, Vedad Hadzic, Uwe Egly, Florian Lonsing, Martina Seidl |
| 2017 | CADE | DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL. | Florian Lonsing, Uwe Egly |
| 2016 | SAT | HordeQBF: A Modular and Massively Parallel QBF Solver. | Toms Balyo, Florian Lonsing |
| 2016 | SAT | Q-Resolution with Generalized Axioms. | Florian Lonsing, Uwe Egly, Martina Seidl |
| 2015 | LPAR | Automated Benchmarking of Incremental SAT and QBF Solvers. | Uwe Egly, Florian Lonsing, Johannes Oetsch |
| 2015 | LPAR | Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination. | Florian Lonsing, Fahiem Bacchus, Armin Biere, Uwe Egly, Martina Seidl |
| 2015 | SAT | Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API. | Florian Lonsing, Uwe Egly |
| 2014 | AISC | Conformant Planning as a Case Study of Incremental QBF Solving. | Uwe Egly, Martin Kronegger, Florian Lonsing, Andreas Pfandler |
| 2014 | CP | Incremental QBF Solving. | Florian Lonsing, Uwe Egly |
| 2014 | FMCAD | SAT-based methods for circuit synthesis. | Roderick Bloem, Uwe Egly, Patrick Klampfl, Robert Knighofer, Florian Lonsing |
| 2014 | SAT | MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing. | Charles Jordan, Lukasz Kaiser, Florian Lonsing, Martina Seidl |
| 2013 | LPAR | Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving. | Uwe Egly, Florian Lonsing, Magdalena Widl |
| 2013 | SAT | Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation. | Florian Lonsing, Uwe Egly, Allen Van Gelder |
| 2012 | CADE | qbf2epr: A Tool for Generating EPR Formulas from QBF. | Martina Seidl, Florian Lonsing, Armin Biere |
| 2012 | SAT | Extended Failed-Literal Preprocessing for Quantified Boolean Formulas. | Allen Van Gelder, Samuel B. Wood, Florian Lonsing |
| 2012 | SAT | Resolution-Based Certificate Extraction for QBF - (Tool Presentation). | Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, Armin Biere |
| 2011 | CADE | Blocked Clause Elimination for QBF. | Armin Biere, Florian Lonsing, Martina Seidl |
| 2011 | SAT | Failed Literal Detection for QBF. | Florian Lonsing, Armin Biere |
| 2010 | SAT | Automated Testing and Debugging of SAT and QBF Solvers. | Robert Brummayer, Florian Lonsing, Armin Biere |
| 2010 | SAT | Integrating Dependency Schemes in Search-Based QBF Solvers. | Florian Lonsing, Armin Biere |
| 2009 | SAT | A Compact Representation for Syntactic Dependencies in QBFs. | Florian Lonsing, Armin Biere |
| 2008 | SAT | Nenofex: Expanding NNF for QBF Solving. | Florian Lonsing, Armin Biere |