QUANTIFY 2015
      International Workshop on 

    Berlin, Germany, August 1, 2015

   Affiliated to and co-located with: 
         CADE 2015 conference
   Berlin, Germany, August 1-7, 2015

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.


Olaf Beyersdorff, University of Leeds


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


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


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


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.


Accepted extended abstracts are collected in an informal report which will be publicly available at the workshop’s website.


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


  • 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