[SMT-LIB] QUANTIFY'14: Call for Papers

[Martina Seidl]

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

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

              QUANTIFY 2014
                 --------
         1st International Workshop
             on Quantification

       Vienna, Austria, July 18, 2014
         http://vsl2014.at/quantify


     Affiliated to and co-located with:

                IJCAR 2014
     Vienna, Austria, July 19-22, 2014
       http://cs.nyu.edu/ijcar2014/

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

Quantifiers play an important role in language extensions of many
logics. The use of quantifiers often allows for a more succinct
encoding than would be possible without quantifiers. However, the
introduction of quantifiers affects the complexity of the extended
formalism in general. Moreover, theoretical results established for
the quantifier-free formalism typically cannot be directly transferred
to the quantified case. Further, techniques successfully implemented
in reasoning tools for quantifier-free formulas cannot directly be
lifted to a quantified version.

The goal of the 1st International Workshop on Quantification
(QUANTIFY 2014) is to bring together researchers who investigate the
impact of quantification from a theoretical as well as from a practical
point of view. Quantification is a topic in different research areas
such as in SAT in terms of QBF, in CSP in terms of QCSP, in SMT, etc.
This workshop has the aim to provide an interdisciplinary forum where
researchers of various fields may exchange their experiences.

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

Please follow the workshop website at http://vsl2014.at/quantify
for any updates.

April 15 2014: paper submission
May    7 2014: notification of acceptance
July  18 2014: workshop

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

The workshop is concerned with all theoretical and practical aspects
of quantification in logics such as QBF, QCSP, SMT, and theorem
proving.  The topics of interest include (but are not limited to):

- Complexity results

- Encodings with and without quantification and comparisons thereof

- Applications of quantification

- Implementations of reasoning tools

- Case studies and experimental results

- Intersections between the different research communities working
   working on quantification

- Surveys of state-of-the-art approaches to handling quantification

=================
PAPER SUBMISSIONS
=================

Submissions will be managed via Easychair:

https://www.easychair.org/conferences/?conf=quantify2014

Submitted papers should be formatted in either LNCS format or a
standard LaTeX article format (paper size A4, font size 11pt).

We solicit two types of submissions:

1. Talk abstracts (maximum two pages, excluding references)
describing already published results.

2. Full papers (maximum 14 pages, excluding references) on novel,
unpublished work.

The talk abstracts of category 1 should include a relevant
bibliography of related work and an outline of the planned talk.
For this category, we explicitly advocate talks which survey results
already published, maybe in multiple articles or presentations
capturing the commonalities and differences
of various quantification approaches (perhaps even interdisciplinary).

Each submission will be assessed by the program committee and 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 reviewers.

Previously published work or extensions thereof may be submitted to the
workshop but that case has to be explicitly stated in the submitted
paper. 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 abstracts and papers are expected to give a talk at
the workshop.

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

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

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

Hubie Chen
Universidad del País Vasco and Ikerbasque, Donostia-San Sebastián, Spain

Florian Lonsing
Vienna University of Technology, Austria

Martina Seidl
Johannes Kepler University Linz, Austria

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

Albert Atserias (Universitat Politecnica de Catalunya)
Nikolaj Bjorner (Microsoft Research)
Mikolas Janota (INESC-ID Lisboa)
Hans Kleine Büning (University of Paderborn)
Konstantin Korovin (Manchester University)
Laura Kovacs (Chalmers University of Technology)
Francesco Scarcello (DIMES, University of Calabria)
Christoph M. Wintersteiger (Microsoft Research)