[SMT-LIB] QBF 2016: Call for Papers

[Florian Lonsing]

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

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

                 QBF 2016
                 --------
        4th International Workshop on
   Quantified Boolean Formulas (and Beyond)

       Bordeaux, France, July 4, 2016
         http://fmv.jku.at/qbf16/


      Affiliated to and co-located with:
            SAT 2016 conference
      Bordeaux, France, July 5-8, 2016
----------------------------------------------------------------------

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 could be
encoded in QBF. Considerable progress has been made in the theory and
practice of QBF solving throughout the past years.

As the efforts of extending languages with quantifiers have not only
been made for propositional logic in terms of QBFs, but in many other
formalism like Constraint Satisfaction Problem (CSP) and
Satisfiability Modulo Theories (SMT), QBF 2016 also targets
researchers working in these related fields in order to exchange
experiences and ideas.

The goal of the International Workshop on Quantified Boolean Formulas
(and Beyond) is to bring together researchers working on theoretical
and practical aspects of QBF solving and related formalisms involving
quantifiers. The workshop addresses theoreticians and practitioners in
order to reflect on the state of the art in research and to
consolidate on immediate and long-term challenges.

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

Please follow http://fmv.jku.at/qbf16/ for any updates.

April     20 2016: paper submission
May       23 2016: notification of acceptance
June      20 2016: camera-ready version of papers
July       4 2016: 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

================
PAPER SUBMISSION
================

Submissions of papers will be managed via Easychair:
https://easychair.org/conferences/?conf=qbf2016

We solicit paper submissions in the following categories:

- talk-only papers: 2-4 pages
- full papers: up to 12 pages
- short tutorial presentation: 2-4 pages

Page limits do not include references and optional appendices.

Talk-only papers present work that has been published already, novel
unpublished work, or work in progress. We explicitly solicit the
submission of talk-only papers describing work that has been published
at other venues and which falls into the scope of the workshop.

Full papers describe novel, unpublished work, including work in
progress.

Authors are encouraged to provide additional material such as source
code of tools, experimental data, benchmarks and related publications.

We plan to publish the accepted papers (except talk-only papers) in
CEUR workshop proceedings, which are indexed with an ISSN.

NEW: we solicit 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.

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.

Previously published work or extensions thereof may be submitted to
the workshop but that case has to be explicitly stated in the
submitted paper. This regulation also applies to work which is
currently under review elsewhere.

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

A short abstract of each talk given at the workshop will be published
on the workshop webpage.

==============
PROGRAM CHAIRS
==============

Florian Lonsing
Vienna University of Technology, Austria

Martina Seidl
Johannes Kepler University Linz, Austria

=================
PROGRAM COMMITTEE
=================

Fahiem Bacchus, University of Toronto, Canada
Olaf Beyersdorff, University of Leeds, UK
Jasmin Christian Blanchette, Inria Nancy and LORIA, France
Hubie Chen, Universidad del Pais Vasco and Ikerbasque, Spain
Marijn Heule, The University of Texas at Austin, USA
Jie-Hong Roland Jiang, National Taiwan University, Taiwan
Friedrich Slivovsky, TU Wien, Austria