CFP (deadline extension) - 6th International Workshop on Quantified Boolean Formulas and Beyond

     CALL FOR PAPERS (EXTENDED DEADLINE): QBF 2019
            
     International Workshop on Quantified Boolean Formulas and Beyond

     Lisbon, Portugal, July 7, 2019. http://fmv.jku.at/qbf19/ 

     Affiliated to and co-located with: SAT'19, Lisbon, Portugal, July 7-12, 2019

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 the 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 could be encoded as a QBF in a natural way. Considerable progress has been made in QBF solving throughout the past years. However, in contrast to SAT, QBF is not yet widely applied to practical problems in academic or industrial settings. For example, the extraction and validation of models of (un)satisfiability of QBFs has turned out to be challenging, given that state-of-the-art solvers implement different solving paradigms.

The goal of the International Workshop on Quantified Boolean Formulas and Beyond (QBF 2019) 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.

The workshop also welcomes work on reasoning with quantifiers in related problems, such as dependency QBF (DQBF), quantified constraint satisfaction problems (QCSP), and satisfiability modulo theories (SMT) with quantifiers.

Invited Speaker

Alexander Feldman, PARC

Important Dates

May 25: Submission (extended deadline)
June 5: Notification (extended deadline)
June 15: Camera-ready versions

Please see the workshop webpage for any updates.

Call for Contributions

The workshop is concerned with all aspects of current research on all formalisms enriched by quantifiers, and in particular QBF. The topics of interest include (but are not limited to):

Applications, encodings and benchmarks with quantifiers
QBF proof theory and complexity results
Certificates and proofs for QBF, QCSP, SMT with quantifiers, etc.
Experimental evaluations of solvers or related tools
Case studies illustrating the power of quantifiers
Formats of proofs and certificates
Implementations of proof checkers and verifiers
Decision procedures
Calculi and their relationships
Data structures, implementation details and heuristics
Pre- and inprocessing techniques
Structural reasoning

Submission

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

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

In particular, we invite the submission of extended abstracts on work that has been published already, novel unpublished work, or work in progress.

The following forms of submissions are solicited:

Proposals for short tutorial presentations on topics related to the workshop. The number of accepted tutorials depends on the overall number of accepted papers and talks, with the aim to set up a balanced workshop program.
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 or related formalisms in various domains are particularly welcome. Additionally, this call comprises known applications that 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 1-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. The workshop does not have formal proceedings.

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