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

----------------------------------------------------------------------
             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.