[SMT-LIB] QBF 2013: Deadline Extension

[Martina Seidl]

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


The QBF Workshop held at the SAT conference in Helsinki 
still invites presentations on QBF related topics!

We solicit any kinds of contributions which are of interest 
to the QBF community ranging from experience reports on 
fully evaluated approaches to radical and innovative ideas. 

If you are interested to contribute, please submit an extended 
abstract (up to LNCS 4 pages) describing the outline 
of your talk.

Deadline is May, 8th. 

Please find below the full call for contributions. 

With kind regards,
Florian Lonsing, Martina Seidl 

------------------------------------------------------------------------
            CALL FOR Contributions

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

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. The workshop also targets
researchers working with quantifiers in other formalisms like Constraint
Satisfaction Problems (CSP) and Satisfiability Modulo Theories (SMT) 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
================================

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.

Please see the submission website for further guidelines:

http://fmv.jku.at/qbf2013/submission.html

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