VSL 2014: VIENNA SUMMER OF LOGIC 2014
QBF Call for Papers

QBF 2014 – Second International Workshop on Quantified Boolean Formulas
July 13, 2014 · Vienna, Austria

http://vsl2014.at/qbf

Also available as pdf file

Important Dates

Submission of extended abstracts: extended deadline (firm): April 25, 2014
Notification of acceptance: May 7, 2014
Workshop July 13, 2014
   

Aims and Scope

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 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 Second International Workshop on Quantified Boolean Formulas (QBF 2014) 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 QBF workshop 2014 is a follow-up edition of the QBF workshop which was held in 2013 in the context of the SAT conference in Helsinki, Finland. The first edition of the workshop in 2013 was attended by 40 participants, which demonstrates the renewed interest in QBF across different research fields.

The QBF Workshop 2014 will include a presentation of the QBF Gallery 2014, a competitive evaluation of QBF solvers and related tools:

http://qbf.satisfiability.org/gallery/

Paper Submissions

Submissions of extended abstracts are solicited and will be managed via Easychair: https://www.easychair.org/conferences/?conf=qbf2014

Submitted extended abstracts should have a maximum overall length of 4 pages in either LNCS format or a standard LaTeX article format (paper size A4, font size 11pt) excluding references.

Each submission will be assessed by the workshop organizers with respect to novelty, originality, and scope.

Submissions related to completed work as well as work in progress are welcome. Authors are encouraged to provide additional material such as source code of tools, experimental data, benchmarks and related publications in an appendix or a related webpage. The additional material will be considered at the discretion of the workshop organizers.

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. Reports on ongoing research are particularly welcome.

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

Since the workshop does not have official proceedings, work related to accepted submissions can be resubmitted to other venues without restrictions.

Authors of accepted extended abstracts are expected to give a talk at the workshop. Accepted extended abstracts are collected in an informal report which will be publicly available at the workshop's website.

Program Committee