[SMT-LIB] QUANTIFY 2015: Call for Papers

[Florian Lonsing]

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

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

                QUANTIFY 2015
                   --------
           International Workshop on
                QUANTIFICATION

         Berlin, Germany, August 1, 2015
http://fmv.jku.at/quantify15/


        Affiliated to and co-located with:
              CADE 2015 conference
        Berlin, Germany, August 1-7, 2015
http://conference.mi.fu-berlin.de/cade-25/home
----------------------------------------------------------------------

Quantifiers play an important role in language extensions of many
logics.  The use of quantifiers often allows for a more succinct
encoding as it would be possible without quantifiers. However, the
introduction of quantifiers affects the complexity of the extended
formalism in general.  Consequently, theoretical results established
for the quantifier-free formalism may not directly be 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 2nd International Workshop on Quantification (QUANTIFY
2015) 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.

===============
INVITED SPEAKER
===============

Olaf Beyersdorff, University of Leeds

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

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

May    8 2015: paper submission
May   29 2015: notification of acceptance
June  23 2015: camera-ready version of papers
August 1 2015: 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 on
   quantification
- Surveys of state-of-the-art approaches to handling quantification

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

Submissions of extended abstracts are solicited and will be managed
via Easychair:

https://easychair.org/conferences/?conf=quantify15

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 extended abstracts are collected in an informal report which
will be publicly available at the workshop's website.

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

Hubie Chen, Universidad del Pais Vasco and Ikerbasque
Florian Lonsing, Vienna University of Technology, Austria
Martina Seidl, Johannes Kepler University Linz, Austria

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

Olaf Beyersdorff, University of Leeds
Nikolaj Bjorner, Microsoft Research
Jasmin Blanchette, TU Munich
Mikolas Janota, INESC-ID Lisboa
Laura Kovacs, Chalmers University of Technology
Francesco Scarcello, DIMES, University of Calabria
Christoph Wintersteiger, Microsoft Research