[SMT-LIB] QBF 2014: Call for Contributions

[Martina Seidl]

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

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

QBF 2014
         
2nd International Workshop on
Quantified Boolean Formulas

Vienna, Austria, July 13, 2014
http://vsl2014.at/qbf

------------------------------------------------------------------------


Affiliated to and co-located with:

SAT 2014 conference
Vienna, Austria, July 14-17, 2014
http://baldur.iti.kit.edu/sat2014/

Vienna Summer of Logic 2014
http://vsl2014.at/

------------------------------------------------------------------------


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/


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

Please follow http://vsl2014.at/qbf for any updates.

April 15 2014: submission of extended abstracts
April 30 2014: notification of acceptance
July  13 2014: workshop


==================
TOPICS OF INTEREST
==================

The workshop is concerned with all aspects of current research on QBF.  The
topics of interest include (but are not limited to):

- QBF applications, encodings, and benchmarks

- Applications of QBF in other formalisms which use quantifiers such as
  quantified constraint satisfaction problems (QCSP) or Satisfiability Modulo
  Theories (SMT)

- Case studies and experimental evaluations

- Certificates and proofs for QBF

- Formats of proofs and certificates

- Implementations of proof checkers and verifiers

- Decision procedures for QBF

- Calculi for QBF

- Data structures, implementation details, and heuristics

- Pre- and inprocessing techniques

- Structural QBF solving


================================
SUBMISSION OF EXTENDED ABSTRACTS
================================

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.


===============
WORKSHOP REPORT
===============

Accepted extended abstracts are collected in an informal report which will be
publicly available at the workshop's website.


===================
WORKSHOP ORGANIZERS
===================

Charles Jordan
Hokkaido University, Sapporo, Japan

Florian Lonsing
Vienna University of Technology, Austria

Martina Seidl
Johannes Kepler University Linz, Austria