Florian Lonsing
e-mail:
"fml" followed by the at-sign and "florianlonsing.com"
WWW:
http://www.florianlonsing.com/
Home
Publications
Software
Talks
Talks
In reverse chronological ordering:
2022
Pono: An SMT-Based Model Checker
.
Center for Automated Reasoning at Stanford University
,
Annual Meeting
.
2021
Invited
tutorial on QBF solving
, jointly with
Martina Seidl
, in the
Beyond Satisfiability Workshop
, part of the
Satisfiability: Theory, Practice, and Beyond
program at the
Simons Institute
.
2020
A Theoretical Framework for Symbolic Quick Error Detection,
SystemX November Conference 2020
, Stanford, CA, USA, online event.
Revised slide deck (PDF)
and
video recording
.
A Theoretical Framework for Symbolic Quick Error Detection,
Stanford Software Research Lunch
, Stanford, CA, USA, online event.
A Theoretical Framework for Symbolic Quick Error Detection,
FMCAD'2020
, online event.
Long talk slides (PDF)
,
video recording of long talk
,
short talk slides (PDF)
.
2019
Unlocking the Power of Formal Hardware Verification with CoSA and Symbolic QED,
SystemX November Conference 2019
, Stanford, CA, USA.
Unlocking the Power of Formal Hardware Verification with CoSA and Symbolic QED
,
ICCAD'2019
, Westminster, CO, USA.
Unlocking the Power of Formal Hardware Verification with CoSA and Symbolic QED,
Stanford Software Research Lunch
, Stanford, CA, USA.
QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties>,
SAT'2019
, Lisbon, Portugal.
Contribution to tutorial:
Pre-silicon Verification & Post-Silicon Validation: An End-to-End Approach with Industrial Applications,
DAC'2019
, Las Vegas, NV, USA.
2018
Evaluating QBF Solvers: Quantifier Alternations Matter
,
CP'2018
, Lille, France.
QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property
,
CiE 2018
, Kiel, Germany; slightly extended version of IJCAR 2018 talk;
related paper
at IJCAR 2018.
QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property
,
IJCAR 2018
, part of
FLoC
, Oxford, UK.
Submissions to QBFEVAL'18
,
QBF Workshop 2018
, affiliated to
SAT 2018
, part of
FLoC
, Oxford, UK.
2017
An Introduction to QBF Solving
,
The Second Indian SAT+SMT School
, Mysuru, India.
Evaluating QBF Solvers: Quantifier Alternations Matter,
AVM'2017
, Visegrad, Hungary.
DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL
,
CADE'2017
, Gothenburg, Sweden.
Parallel QBF Solving: State of the Art Techniques and Future Perspectives
,
PCR'2017
, Gothenburg, Sweden.
2016
An Overview of QBF Reasoning Techniques
,
SAT and Interactions
, Schloss Dagstuhl, Leibniz-Zentrum fuer Informatik.
Solving (Problems with) Quantified Boolean Formulas: Recent Trends and Challenges
,
IJCAI-16
, New York City, USA.
Q-Resolution with Generalized Axioms
,
SAT'2016
, Bordeaux, France.
Submissions to QBFEVAL'16
,
QBF'2016
, Bordeaux, France.
Advances in QBF Reasoning
,
SAT/SMT/AR Summer School 2016
, Lisbon, Portugal.
2015
Automated Benchmarking of Incremental SAT and QBF Solvers
,
LPAR 2015
, Suva, Fiji.
Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination
,
LPAR 2015
, Suva, Fiji.
Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination.
PUMA/RiSE Workshop 2015
, Bad Griesbach, Germany.
Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
,
SAT'2015
, Austin, Texas, USA.
2014
Conformant Planning as a Case Study of Incremental QBF Solving
,
AISC 2014
, Sevilla, Spain.
Incremental QBF Solving
,
CP 2014
, Lyon, France.
Incremental QBF Solving by DepQBF,
ICMS 2014
, Seoul, South Korea.
MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing
,
SAT'2014
, Vienna, Austria.
Incremental QBF Solving,
AVM'2014
, Frejus, France.
Inside Search-Based QBF Solvers
and
DepQBF in Practice
, at the
ReRiSE'14 Winter School
, Johannes Kepler University, Linz, Austria.
2013
Search-based QBF Solving: Basics, Recent Trends and Challenges.
JST ERATO Minato Discrete Strucure Manipulation System Project Seminar
, Hokkaido University, Sapporo, Japan. October 2013.
The QBF Gallery 2013
,
SAT'13
, Helsinki, Finnland.
The QBF Gallery 2013
,
QBF Workshop 2013
, Helsinki, Finnland.
Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
,
SAT'13
, Helsinki, Finnland.
2012
QBF Certificates: Challenges and Future Research Directions.
PUMA/RiSE Workshop 2012
, Goldegg, Salzburg, Austria.
2011
Blocked Clause Elimination for QBF
,
CADE'11
, Wroclaw, Poland
Failed Literal Detection for QBF
,
SAT'11
, Ann Arbor, Michigan, USA.
Preprocessing QBF: Failed Literals and Quantified Blocked Clause Elimination
,
Deduction at Scale Seminar
, Ringberg Castle, Tegernsee, Germany.
2010
Practical Aspects of Dependency Schemes in QBF Solving
,
AVM'10
, Lugano, Switzerland
Integrating Dependency Schemes in Search-Based QBF Solvers (
Talk
) (
Poster
),
SAT'10
, Edinburgh, Scotland, UK
DepQBF: A Dependency-Aware QBF Solver (System Description)
,
POS'10
, Edinburgh, Scotland, UK.
2009
A Compact Representation for Syntactic Dependencies in QBFs
,
SAT'09
, Swansea, Wales, UK.
2008
Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers
,
MEMICS'08
, Znojmo, Czech Republic
Nenofex: Expanding NNF for QBF Solving
,
SAT'08
, Guangzhou, P. R. China.