[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS] SMT Workshop 2010: 1st call for papers

1st Call for papers
SMT Workshop 2010
International Workshop on Satisfiability Modulo Theories

Affiliated with CAV 2010 and SAT 2010
July 14-15, 2009, Edinburgh


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 others.  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.

Paper Submission and Proceedings

* Original papers contain original research (simultaneous submissions are
not allowed) and sufficient detail to assess the merits and relevance of the

* Presentation-only papers describe work recently published or submitted to
other venues.  We see this as a way to provide additional access to
important developments that SMT Workshop attendees may be unaware of.

Submission is via EasyChair. Papers in both categories will be
peer-reviewed.  Papers should not exceed 10 pages (Postscript or PDF) and
should be written in LaTeX, 11pt, one column, a4paper, standard margins. 
Technical details may be included in an appendix.

Only informal proceedings will be distributed at the workshop. Papers
presented at SMT 2010 in both categories will be considered for one of two
special issues of the following journals, depending on the paper's subject:

* There will be a special issue of FMSD for those papers addressing
  applications of SMT in systems verification.

* There will be a special issue of JSAT for the algorithmic/theory papers.

The selection between FMSD and JSAT will be based on the scope of the paper
prior to the reviewing process.

Important Dates

Submission deadline (strict)   April 2, 2009
Notification                   May 3, 2009
Workshop                       July 14-15, 2009

Workshop Chairs
* Aarti Gupta, NEC Labs America
* Daniel Kroening, Oxford University

Program Committee
* Clark Barrett, New York University
* Armin Biere, Johannes Kepler University Linz
* Nikolaj Bjorner, Microsoft Research
* Alessandro Cimatti, ITC-IRST, Trento
* Leonardo de Moura, Microsoft Research
* Bruno Dutertre, SRI International
* Himanshu Jain, Synopsys
* Sava Krstic, Intel Corporation
* David Monniaux, Verimag
* Philipp Ruemmer, Oxford University
* Roberto Sebastiani, Universita di Trento
* Cesare Tinelli, University of Iowa