[SMT-LIB] QBF 2015: Call for Papers

[Florian Lonsing]

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

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

                 QBF 2015
                 --------
        3rd International Workshop on
         Quantified Boolean Formulas

       Austin, Texas, Sep 23, 2015
         http://fmv.jku.at/qbf15/


      Affiliated to and co-located with:
            SAT 2015 conference
      Austin, Texas, Sep 24-27, 2015
------------------------------------------------------------------------

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 2015) 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 2015 also targets researchers working in
these fields in order to exchange experiences and ideas.

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

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

July      20 2015: paper submission
August    12 2015: notification of acceptance
September 01 2015: camera-ready version of papers
September 23 2015: 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/qbf15/submission.html

Submitted extended abstracts should have an overall length of up to 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.

We explicitly solicit the submission of talk abstracts describing work which
is of interest to the SAT/QBF community and which has been published
at venues other than the QBF workshop or the SAT conference.

Submissions related to completed work as well as work in progress are
welcome which will trigger interesting discussions.
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.

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.

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

Florian Lonsing
Vienna University of Technology, Austria

Martina Seidl
Johannes Kepler University Linz, Austria

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

Armin Biere, University of Linz, Austria
Uwe Egly, Vienna University of Technology, Austria
Mikolas Janota, INESC-ID Lisboa, Portugal
Will Klieber, Carnegie Mellon University, USA
Allen Van Gelder, University of California at Santa Cruz, USA