[SMT-LIB] QBF 2013 Call For Papers

[Florian Lonsing]

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

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

QBF 2013
--------
International Workshop on
Quantified Boolean Formulas

Helsinki, Finland, July 9, 2013
http://fmv.jku.at/qbf2013/


Affiliated to and co-located with:
SAT 2013 conference
Helsinki, Finland, July 8-12, 2013
http://sat2013.cs.helsinki.fi/
------------------------------------------------------------------------

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 International Workshop on Quantified Boolean Formulas
(QBF 2013) 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.

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

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

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

April 24 2013: paper submission
May 20 2013: notification of acceptance
June 15 2013: camera-ready version of papers
July 9 2013: workshop

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

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

- QBF applications, encodings and benchmarks

- 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

- Quantifiers in other formalisms like SMT or CSP

- Tools related to any aspect of QBF/CSP/SMT reasoning

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

Submissions of extended abstracts are solicited and will be managed via
Easychair: http://fmv.jku.at/qbf2013/submission.html

Submitted extended abstracts should have an overall length of 4 pages in
LNCS format excluding references. Authors may decide to include an
appendix with additional material. Appendices will be considered at the
reviewers' discretion.

Submissions related to completed work as well as work in progress are
welcome. Submissions will be reviewed with respect to novelty,
originality and scope. Authors are encouraged to provide additional
material such as source code of tools, experimental data, benchmarks and
related publications.

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.

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

Florian Lonsing
Vienna University of Technology, Austria

Martina Seidl
Johannes Kepler University Linz, Austria

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

Fahiem Bacchus
Armin Biere
Nikolaj Björner
Uwe Bubeck
Hans Kleine Büning
Hubie Chen
Nadia Creignou
Uwe Egly
Allen Van Gelder
Enrico Giunchiglia
Mikoláš Janota
Massimo Narizzano
Stefan Szeider