[bull-ia] Call for papers – QBF 2018

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



QBF 2018


International Workshop on

Quantified Boolean Formulas and Beyond

Oxford, UK, July 8, 2018


Affiliated to and co-located with:

Federated Logic Conference 2018 (FLoC), Oxford, UK

Oxford, UK, July 6-19, 2018


Quantified Boolean formulas (QBF) are an extension of propositional

logic which allows for explicit quantification over propositional

variables. The decision problem of QBF is PSPACE-complete, compared

to NP-completeness of the decision problem of propositional logic (SAT).

Many problems from application domains such as model checking, formal

verification or synthesis are PSPACE-complete, and hence can be

encoded in QBF. Considerable progress has been made in QBF solving

throughout the past years. However, in contrast to SAT, QBF is not

widely applied to practical problems in industrial settings.

For example, the extraction and validation of models of

(un)satisfiability of QBFs has turned out to be challenging.

The goal of the International Workshop on Quantified Boolean Formulas

(QBF Workshop) 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.




We are very pleased to announce that QBF 2018 will feature a

joint session with the Int. Workshop on Proof Complexity (PC 2018).

We cordially invite contributions that are in the intersection

of reasoning with quantifiers and proof complexity.

Further, we are very pleased to announce that

Meena Mahajan will give an invited talk in the joint session.




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

May 01 2018: submission

May 15 2018: notification of acceptance

May 25 2018: camera-ready version

July 8 2018: workshop




The workshop is concerned with all aspects of current research on

formalisms enriched by quantifiers, in particular QBF. The topics of

interest include (but are not limited to):

– Applications, encodings and benchmarks with quantifiers

– Experimental evaluations of solvers or related tools

– Case studies illustrating the power of quantifiers

– Certificates and proofs for QBF, QSMT, QCSP, etc.

– Formats of proofs and certificates

– Implementations of proof checkers and verifiers

– Decision procedures

– Calculi and their relationships

– Proof theory and complexity results

– Data structures, implementation details, and heuristics

– Pre- and inprocessing techniques

– Structural reasoning




We invite the submission of extended abstracts on work that has

been published already, novel unpublished work, or work in progress.

Submissions of the extended abstracts will be managed via Easychair:


The following forms of submissions are solicited:

– Proposals for short tutorial presentations on topics related to the

workshop. Tutorial proposals will be reviewed by the

PC. The number of accepted tutorials depends on the overall number of

accepted papers and talks, with the aim to set up a balanced workshop


– Talk abstracts reporting on already published work.

Such an abstract should include an outline of the planned talk,

and pointers to relevant bibliography.

– Talk proposals presenting work that is unpublished or in progress.

Submissions which describe novel applications of QBF in various

domains are particularly welcome. Additionally, this call comprises

known applications which have been shown to be hard for QBF solvers in

the past as well as new applications for which present QBF solvers

might lack certain features still to be identified.

Each submission should have an overall length of 2-4 pages in LNCS format.

Authors may decide to include an appendix with additional material.

Appendices will be considered at the reviewers’ discretion.

The accepted extended abstracts will be published on the workshop

webpage and on the USB stick of FLoC.

Authors of accepted contributions are expected to give a talk at the





Hubie Chen

Birkbeck, University of London

Florian Lonsing

Vienna University of Technology, Austria

Martina Seidl

Johannes Kepler University Linz, Austria




Florent Capelli

Leroy Chew

Mikolas Janota

Mathias Preiner

Markus Rabe

Martin Suda

Friedrich Slivovsky

Desinscription: envoyez un message a: bull-ia-unsubscribe@gdria.fr
Pour obtenir de l’aide, ecrivez a: bull-ia-help@gdria.fr