Florian Lonsing

62 papers A* 2A 19B 8Misc 1Journal 25Unranked 4

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