[isabelle] 1st CFP: FMSD Special Issue on Satisfiability Modulo Theories

===================  Preliminary Call for Papers =====================

Journal on Formal Methods in System Design (FMSD)
Special Issue on Recent Topics in Satisfiability Modulo Theories (SMT)

Deadline for abstract submission (provisional): May 2nd 2016
Deadline for full paper submission (provisional): August 19th 2016



Determining the satisfiability of first-order formulas modulo background
theories, known as the Satisfiability Modulo Theories (SMT) problem, has
proved to be an enabling technology for verification, test-vector
generation, compiler optimization, scheduling, and other areas.

The success of SMT techniques depends on the development of both
domain-specific decision procedures for each concrete theory (e.g.,
linear arithmetic, the theory of arrays, or the theory of bit-vectors)
and combination methods that allow one to obtain more versatile SMT
tools. These two ingredients together make SMT techniques well-suited
for use in larger automated reasoning and formal verification efforts.

(See also the SMT-LIB page http://www.smtlib.org/, and the page of the
annual SMT Workshop http://www.smt-workshop.org/)


The goal of the special issue is to survey recent developments in the
SMT field. Topics of interest include, but are not restricted to:

- Novel general SMT techniques
- New decision procedures and new theories of interest
- Construction of models, proofs, interpolants, etc.
- Techniques for handling quantifiers
- Combinations of decision procedures
- Novel implementation techniques
- Benchmarks and evaluation methodologies
- Formats for new theories, and developments in SMT-LIB
- Applications and case studies
- Theoretical results


This special issue welcomes original high-quality contributions that
have been neither published in nor submitted to any journals or refereed
conferences. Extended versions of conference papers should include at
least 30% of new material.

All submissions should be written in terms understandable by general
readers of the journal. To simplify the publication process, there will
be a two step selection process. Authors willing to submit to this
special issues are asked to send an abstract (of at most 1 page)
describing the intended contribution. We will then select most promising
abstracts and will ask the authors to submit a full version. The full
version of all submissions will be refereed according to FMSD standards,
as described at FMSD web page (see below). Note that acceptance of the
abstract does not guarantee acceptance of the full version. The guest
editors reserve the right to invite further relevant papers, including
extended versions of papers that appeared at recent workshops or

Abstracts should be submitted via email to the guest editors.
Manuscripts should be submitted in LaTeX according to FMSD's author
guidelines. Please use Springer's LaTeX macro package and choose the
formatting option "smallcondensed". Submissions should not exceed 30
pages. FMSD LaTeX style file can be obtained at the journal web page
(see below).


Formal Methods in System Design reports on the latest formal methods for
designing, implementing, and validating the correctness of hardware
(VLSI) and software systems. Readers will find high quality, original
papers describing all aspects of research and development. Contributions
to the journal serve its goal of developing an important and highly
useful collection of commonly applicable formal methods that will
strongly influence future design environments and design methods. For
more information, see the journal webpage at


- Abstract submission deadline: May 2nd 2016
- Abstract acceptance notification: May 15th 2016
- Full paper submission deadline: August 19th 2016
- Prospective publication of the issue: Spring 2017


Alberto Griggio, Fondazione Bruno Kessler <griggio at fbk.eu>
Philipp Ruemmer, Uppsala University <philipp.ruemmer at it.uu.se>


For further information, send an email to one of the guest editors.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.