[SMT-LIB] QUANTIFY 2015: Deadline Extension

[Florian Lonsing]

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

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

       QUANTIFY 2015 - DEADLINE EXTENSION!
                   --------
           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   24 2015: paper submission (EXTENDED DEADLINE)
June   7 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.

Please see the workshop website for a full description of the paper
categories and submission instructions.

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