[SMT-LIB] QBF 2014: Deadline Extension

[Martina Seidl]

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

------------------------------------------------------------------------
   FINAL CALL FOR PAPERS (DEADLINE EXTENDED)

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

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 and applications. 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 the workshop website at http://vsl2014.at/qbf for any updates.

April 25 2014: submission of extended abstracts [DEADLINE EXTENDED]
May    7 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
================================

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.

Please see the workshop website for further submission guidelines:

http://vsl2014.at/qbf

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