QBF Workshop 2019: Final Call for Papers

[HUBERT MING CHEN]

[We apologize if you receive multiple copies of this call]

----------------------------------------------------------------------
              CALL FOR PAPERS

                 QBF 2019
                 --------
          International Workshop on
   Quantified Boolean Formulas and Beyond

       Lisbon, Portugal, July 7, 2019
         http://fmv.jku.at/qbf19/

   Affiliated to and co-located with:
  Int. Conf. on Theory and Applications
   of Satisfiability Testing (SAT'19)
    Lisbon, Portugal, July 7-12, 2019
----------------------------------------------------------------------

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
the 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 as a QBF in a natural way. Considerable progress has been made
in QBF solving throughout the past years. However, in contrast to SAT,
QBF is not yet widely applied to practical problems in academic or
industrial settings. For example, the extraction and validation of
models of (un)satisfiability of QBFs has turned out to be
challenging, given that state-of-the-art solvers implement different
solving paradigms.

The goal of the International Workshop on Quantified Boolean Formulas
and Beyond (QBF 2019) 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.

The workshop also welcomes work on reasoning with quantifiers in
related problems, such as dependency QBF (DQBF), quantified constraint
satisfaction problems (QCSP), and satisfiability modulo theories (SMT)
with quantifiers.

===============
INVITED SPEAKER
===============

Alexander Feldman, PARC

===============
IMPORTANT DATES
===============

May  25: Submission (extended)
June  5: Notification (extended)
June 15: Camera-ready versions

Please see the workshop webpage for any updates:
  http://fmv.jku.at/qbf19/

======================
CALL FOR CONTRIBUTIONS
======================

The workshop is concerned with all aspects of current research on all
formalisms enriched by quantifiers, and in particular QBF. The topics
of interest include (but are not limited to):

- Applications, encodings and benchmarks with quantifiers
- QBF proof theory and complexity results
- Certificates and proofs for QBF, QCSP, SMT with quantifiers, etc.
- Experimental evaluations of solvers or related tools
- Case studies illustrating the power of quantifiers
- Formats of proofs and certificates
- Implementations of proof checkers and verifiers
- Decision procedures
- Calculi and their relationships
- Data structures, implementation details and heuristics
- Pre- and inprocessing techniques
- Structural reasoning

==========
SUBMISSION
==========

Submissions of extended abstracts are invited and will be managed via
Easychair:

https://easychair.org/conferences/?conf=qbf19

In particular, we invite the submission of extended abstracts on work
that has been published already, novel unpublished work, or work in
progress.

The following forms of submissions are solicited:

- Proposals for short tutorial presentations on topics related to the
   workshop. 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 or related
   formalisms in various domains are particularly welcome.
   Additionally, this call comprises known applications that 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 1-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. The workshop does not have formal proceedings.

Authors of accepted contributions are expected to give a talk at the
workshop.

=======
CONTACT
=======

qbf19 at easychair.org

===============================
PROGRAM CHAIRS AND ORGANIZATION
===============================

Hubie Chen, Birkbeck, University of London
Florian Lonsing, Stanford University
Martina Seidl, University of Linz, Austria
Friedrich Slivovsky, TU Wien, Austria