posted by user: mseidl || 1834 views || tracked by 5 users: [display]

QBF 2013 : International Workshop on Quantified Boolean Formulas


When Jul 9, 2013 - Jul 9, 2013
Where Helsinki
Submission Deadline Apr 24, 2013
Notification Due May 20, 2013
Final Version Due Mar 6, 2014
Categories    computer science

Call For Papers


QBF 2013
International Workshop on
Quantified Boolean Formulas

Helsinki, Finland, July 9, 2013

Affiliated to and co-located with:
SAT 2013 conference
Helsinki, Finland, July 8-12, 2013

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 could 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 and has turned out to be challenging.

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

As the efforts of extending languages with quantifiers have not only be
made for propositional logic in terms of QBFs, but in many other
formalism like Constraint Satisfaction Problem (CSP) and Satisfiability
Modulo Theories (SMT), QBF 2013 also targets researchers working in
these fields in order to exchange experiences and ideas.


Please follow for any updates.

April 24 2013: paper submission
May 20 2013: notification of acceptance
June 15 2013: camera-ready version of papers
July 9 2013: workshop


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

- QBF applications, encodings and benchmarks
- Case studies and experimental evaluations
- Certificates and proofs for QBF
- Formats of proofs and certificates
- Implementations of proof checkers and verifiers
- Decision procedures for QBF
- Calculi for QBF- Data structures, implementation details and heuristics
- Pre- and inprocessing techniques
- Structural QBF solving
- Quantifiers in other formalisms like SMT or CSP
- Tools related to any aspect of QBF/CSP/SMT reasoning


Submissions of extended abstracts are solicited and will be managed via

Submitted extended abstracts should have an overall length of 4 pages in
LNCS format excluding references. Authors may decide to include an
appendix with additional material. Appendices will be considered at the
reviewers' discretion.

Submissions related to completed work as well as work in progress are
welcome. Submissions will be reviewed with respect to novelty,
originality and scope. Authors are encouraged to provide additional
material such as source code of tools, experimental data, benchmarks and
related publications.

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. Reports on ongoing
research are particularly welcome.

Previously published work or extensions thereof may be submitted to the
workshop but that case has to be explicitly stated in the extended
abstract. 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

Authors of accepted extended abstracts 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.


Florian Lonsing
Vienna University of Technology, Austria

Martina Seidl
Johannes Kepler University Linz, Austria


Fahiem Bacchus
Armin Biere
Nikolaj Björner
Uwe Bubeck
Hans Kleine Büning
Hubie Chen
Nadia Creignou
Uwe Egly
Allen Van Gelder
Enrico Giunchiglia
Mikoláš Janota
Massimo Narizzano
Stefan Szeider

Related Resources

iWOAR 2020   iWOAR 2020 – 7th international Workshop on Sensor-based Activity Recognition and Interaction
ACM--NLPIR--Ei Compendex and Scopus 2020   ACM--2020 4th International Conference on Natural Language Processing and Information Retrieval (NLPIR 2020)--Scopus, Ei Compendex
MART 2020   CALL FOR TASK PARTICIPATION: MART (Micro Activity Retrieval Task) at NTCIR-15 (June 30th deadline)
RiE 2021   12th International Conference on Robotics in Education
AIP Journal - Indexed in Scopus 2021   Journal of Social and Business Informatics - Acta Informatica Pragensia
FCSIT 2020   2020 2nd Euro-Asia Conference on Frontiers of Computer Science and Information Technology (FCSIT 2020)
ACM--ICMLSC--EI Compendex, Scopus 2021   ACM--2021 The 5th International Conference on Machine Learning and Soft Computing (ICMLSC 2021)--EI Compendex, Scopus
IEEE--ICCCR--Ei Compendex, Scopus 2021   IEEE--2021 International Conference on Computer, Control and Robotics (ICCCR 2021)--Ei Compendex, Scopus
SESBC 2020   International Conference on Software Engineering, Security and Blockchain
ACM-ACAI 2020-Ei/Scopus 2020   2020 3rd International Conference on Algorithms, Computing and Artificial Intelligence (ACAI 2020)