QBF Home Page
July 13, 2014 · Vienna, Austria
co-located with the
17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014)
News
- Registration is open: http://vsl2014.at/registration/
- The workshop program is available, including talk abstracts.
Talks
The workshop program consists of contributed talks, which are related to papers accepted at the workshop, and invited talks. The topics of the talks cover areas of ongoing research where considerable progress has been made recently, such as preprocessing, new calculi, proof complexity results, certificate generation, applications, and dependency quantified Boolean formulas (DQBF).
Additionally, the QBF Gallery 2014, which is part of the FLoC Olympic Games, will be presented at the workshop.
Invited Talks
- Marijn Heule: A Unified Proof System for QBF Preprocessing
- Mikolas Janota: On Instantiation-Based Calculi for QBF
- Christoph Scholl: Dependency Quantified Boolean Formulas - Challenges, Applications, First Lines of Attack
- Paolo Marin, Christian Miller and Bernd Becker: Incremental QBF Reasoning for the Verification of Partial Designs
- Robert Koenighofer: Reactive Synthesis using (Incremental) QBF Solving
- Martin Kronegger, Andreas Pfandler, Florian Lonsing and Uwe Egly: Conformant Planning as a Case Study of Incremental QBF Solving
- Adrià Gascón: Synthesis of distributed systems using QBF
Contributed Talks
- Uwe Egly: On the Relation between Resolution Calculi for QBFs and First-order Formulas
- Friedrich Slivovsky and Stefan Szeider: Resolution Paths and Term Resolution
- Valeriy Balabanov, Jie-Hong Roland Jiang, Mikoláš Janota and Magdalena Widl: Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs
Overview
Quantified Boolean formulas (QBF) are an extension of propositional logic
which allows for explicit quantification over propositional variables. The
decision problem of QBF is PSPACE-complete compared to NP-completeness
which allows for explicit quantification over propositional variables. The
decision problem of QBF is PSPACE-complete compared to NP-completeness
of the decision problem of propositional logic (SAT).
Many problems from application domains such as model checking, formal
verification or synthesis are PSPACE-complete, and hence could be encoded in
QBF. Considerable progress has been made in QBF solving throughout the past
years. However, in contrast to SAT, QBF is not widely applied to practical
problems in industrial settings. For example, the extraction and validation of
models of (un)satisfiability of QBFs and has turned out to be challenging.
The goal of the International Workshop on Quantified Boolean Formulas (QBF
Workshop) is to bring together researchers working on theoretical and
practical aspects of QBF solving. In addition to that, it addresses
(potential) users of QBF in order to reflect on the state-of-the-art and to
consolidate on immediate and long-term research challenges.
In particular, the following topics shall be considered at the workshop:
Many problems from application domains such as model checking, formal
verification or synthesis are PSPACE-complete, and hence could be encoded in
QBF. Considerable progress has been made in QBF solving throughout the past
years. However, in contrast to SAT, QBF is not widely applied to practical
problems in industrial settings. For example, the extraction and validation of
models of (un)satisfiability of QBFs and has turned out to be challenging.
The goal of the International Workshop on Quantified Boolean Formulas (QBF
Workshop) is to bring together researchers working on theoretical and
practical aspects of QBF solving. In addition to that, it addresses
(potential) users of QBF in order to reflect on the state-of-the-art and to
consolidate on immediate and long-term research challenges.
In particular, the following topics shall be considered at the workshop:
- Directions of Solver Development
- Certificates
- Applications
- Community Platform and Repository
Previous Edition
The first edition of the QBF Workshop took place in 2013 and was affiliated to SAT 2013 held in Helsinki, Finland.
Call for Papers
http://vsl2014.at/pages/QBF-cfp.html
Organization
- Charles Jordan (Hokkaido University) - chair
- Florian Lonsing (Vienna University of Technology) - chair
- Martina Seidl (Johannes Kepler University Linz) - chair