----------------------------------------------------------------------
CALL FOR PAPERS
QBF 2018
--------
International Workshop on
Quantified Boolean Formulas and Beyond
Oxford, UK, July 8, 2018
http://fmv.jku.at/qbf18/
Affiliated to and co-located with:
Federated Logic Conference 2018 (FLoC), Oxford, UK
Oxford, UK, July 6-19, 2018
----------------------------------------------------------------------
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 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 can 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 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
===============
IMPORTANT DATES
===============
Please follow http://fmv.jku.at/qbf18/ for any updates.
May 01 2018: submission
May 15 2018: notification of acceptance
May 25 2018: camera-ready version
July 8 2018: workshop
==================
TOPICS OF INTEREST
==================
The workshop is concerned with all aspects of current research on
formalisms enriched by quantifiers, in particular QBF. The topics of
interest include (but are not limited to):
- Applications, encodings and benchmarks with quantifiers
- Experimental evaluations of solvers or related tools
- Case studies illustrating the power of quantifiers
- Certificates and proofs for QBF, QSMT, QCSP, etc.
- Formats of proofs and certificates
- Implementations of proof checkers and verifiers
- Decision procedures
- Calculi and their relationships
- Proof theory and complexity results
- Data structures, implementation details, and heuristics
- Pre- and inprocessing techniques
- Structural reasoning
==========
SUBMISSION
==========
We invite the submission of extended abstracts on work that has
been published already, novel unpublished work, or work in progress.
Submissions of the extended abstracts will be managed via Easychair:
https://easychair.org/conferences/?conf=qbf18
The following forms of submissions are solicited:
- Proposals for short tutorial presentations on topics related to the
workshop. Tutorial proposals will be reviewed by the
PC. The number of accepted tutorials depends on the overall number of
accepted papers and talks, with the aim to set up a balanced workshop
program.
- Talk abstracts reporting on already published work.
Such an abstract should include an outline of the planned talk,
and pointers to relevant bibliography.
- Talk proposals presenting work that is unpublished or in progress.
Submissions which describe novel applications of QBF in various
domains are particularly welcome. Additionally, this call comprises
known applications which have been shown to be hard for QBF solvers in
the past as well as new applications for which present QBF solvers
might lack certain features still to be identified.
Each submission should have an overall length of 2-4 pages in LNCS format.
Authors may decide to include an appendix with additional material.
Appendices will be considered at the reviewers' discretion.
The accepted extended abstracts will be published on the workshop
webpage and on the USB stick of FLoC.
Authors of accepted contributions are expected to give a talk at the
workshop.
==========================
JOINT SESSION WITH PC 2018
==========================
We are very pleased to announce that QBF 2018 will feature a
joint session with the Int. Workshop on Proof Complexity (PC 2018).
We cordially invite contributions that are in the intersection
of reasoning with quantifiers and proof complexity.
Further, we are very pleased to announce that
Meena Mahajan will give an invited talk in the joint session.
==============
PROGRAM CHAIRS
==============
Hubie Chen
Birkbeck, University of London
Florian Lonsing
Vienna University of Technology, Austria
Martina Seidl
Johannes Kepler University Linz, Austria
=================
PROGRAM COMMITTEE
=================
Florent Capelli
Leroy Chew
Mikolas Janota
Mathias Preiner
Markus Rabe
Martin Suda
Friedrich Slivovsky
**********************************************************
*
* Contributions to be spread via DMANET are submitted to
*
* DMANET@zpr.uni-koeln.de
*
* Replies to a message carried on DMANET should NOT be
* addressed to DMANET but to the original sender. The
* original sender, however, is invited to prepare an
* update of the replies received and to communicate it
* via DMANET.
*
* DISCRETE MATHEMATICS AND ALGORITHMS NETWORK (DMANET)
* http://www.zaik.uni-koeln.de/AFS/publications/dmanet/
*
**********************************************************
Posts
