[isabelle] SMT 2014: Call for papers

--- 1st CALL FOR PAPERS ---

(We apologize if you receive multiple copies of this message)


SMT Workshop 2014

12th International Workshop on Satisfiability Modulo Theories

Affiliated with CAV, IJCAR, and SAT at FLoC 2014

July 17-18, 2014
Vienna, Austria




Determining the satisfiability of first-order formulas modulo
background theories, known as the Satisfiability Modulo Theories (SMT)
problem, has proven to be an enabling technology for verification,
synthesis, test generation, compiler optimization, scheduling, and
other areas. The success of SMT techniques depends on the development
of both domain-specific decision procedures for each background 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, usually leveraging Boolean satisfiability (SAT)
solvers. These ingredients together make SMT techniques well-suited
for use in larger automated reasoning and verification efforts.

Aims and Scope

The goal of the SMT Workshop is to bring together both researchers and
users of SMT technology and provide them with a forum for presenting
and discussing both new theoretical ideas and implementation and
evaluation techniques. Topics of the workshop include, but are not
limited to:

* Decision procedures and theories of interest
* Combinations of decision procedures
* Novel implementation techniques
* Benchmarks and evaluation methodologies
* Applications and case studies
* Theoretical results

Papers on pragmatic aspects of implementing and using SMT tools, as well
as novel applications of SMT, are especially encouraged.

Important dates

* Submission deadline:       April 13th, 2014
* Notification:              May 20th, 2014
* Camera ready versions due: May 27th, 2014
* Workshop:                  July 17-18, 2014

All dates are "anywhere on earth".

Paper submission and Proceedings

Three categories of submissions are invited:

* Extended abstracts: we strongly encourage the submission of
  preliminary reports of work in progress. They may range in length
  from very short (a couple of pages) to the full 10 pages, and will
  be judged based on the expected level of interest for the SMT
  community. They will be included in the informal proceedings.

* Original papers: contain original research (simultaneous submissions
  are not allowed) and sufficient detail to assess the merits and
  relevance of the submission. For papers reporting experimental
  results, authors are strongly encouraged to make their data

* Presentation-only papers: describe work relevant for the SMT
  community that has recently been published or submitted at other
  venues. They will not be included in the proceedings.

Papers in all three categories will be peer-reviewed. Papers should
not exceed 10 pages, should be prepared in LaTeX using the
easychair.cls class file, and submitted in standard-conforming
PDF. Technical details may be included in an appendix to be read at
the reviewers' discretion.

To submit a paper, go to the EasyChair SMT page
http://www.easychair.org/conferences/?conf=smt20140 and follow the
instructions there.

Program Committee

* Martin Brain (University of Oxford)
* Roberto Bruttomesso (Atrenta)
* Bruno Dutertre (SRI international)
* Pascal Fontaine (Inria, Loria, University of Lorraine)
* Malay Ganai (NEC Labs America)
* Sicun Gao (Carnegie Mellon University)
* Amit Goel (Intel Corporation)
* Alberto Griggio (FBK-IRST)
* Jochen Hoenicke (University of Freiburg)
* Dejan Jovanović (SRI international)
* Albert Oliveras (Technical University of Catalonia)
* Philipp Rümmer (Uppsala University) - co-chair
* Christoph Sticksel (The University of Iowa)
* Cesare Tinelli (The University of Iowa)
* Tjark Weber (Uppsala University)
* Georg Weissenbacher (Vienna University of Technology)
* Thomas Wies (New York University)
* Christoph M. Wintersteiger (Microsoft Research) - co-chair

Attachment: signature.asc
Description: This is a digitally signed message part

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