=================== 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 ====================================================================== GENERAL INFORMATION 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/) TOPICS 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 SUBMISSIONS 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 conferences. 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). ABOUT FMSD 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 http://link.springer.com/journal/10703 PRELIMINARY DATES - 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 GUEST EDITORS Alberto Griggio, Fondazione Bruno Kessler Philipp Ruemmer, Uppsala University FURTHER INFORMATION For further information, send an email to one of the guest editors.