In reverse chronological ordering.
Invited Talks and Tutorials
2021
- Tutorial on QBF solving, jointly with Martina Seidl, in the Beyond Satisfiability Workshop 2021, part of the Satisfiability: Theory, Practice, and Beyond program at the Simons Institute at Berkeley.
2019
- Contribution to tutorial: Pre-silicon Verification & Post-Silicon Validation: An End-to-End Approach with Industrial Applications, DAC’2019, Las Vegas, NV, USA.
2018
- 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.
2017
- An Introduction to QBF Solving, The Second Indian SAT+SMT School 2017, Mysuru, India.
- 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, 2016, Schloss Dagstuhl, Leibniz-Zentrum für Informatik.
- Solving (Problems with) Quantified Boolean Formulas: Recent Trends and Challenges, IJCAI-16, 2016, New York City, USA.
- Advances in QBF Reasoning, SAT/SMT/AR Summer School 2016, Lisbon, Portugal.
2014
- Inside Search-Based QBF Solvers and DepQBF in Practice, at the ReRiSE’14 Winter School, 2014, 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.
2011
- Preprocessing QBF: Failed Literals and Quantified Blocked Clause Elimination , Deduction at Scale Seminar, Ringberg Castle, Tegernsee, Germany, 2011.
Talks at Conferences and Other Venues
2022
- Pono: An SMT-Based Model Checker. Center for Automated Reasoning at Stanford University, Annual Meeting.
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.
2018
- Evaluating QBF Solvers: Quantifier Alternations Matter, CP’2018, Lille, France.
- 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
- 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.
2016
- Q-Resolution with Generalized Axioms, SAT’2016, Bordeaux, France.
- Submissions to QBFEVAL’16, QBF’2016, Bordeaux, France.
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.
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.
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.