The Coq mailing list

[Pascal Fontaine <Pascal.Fontaine AT loria.fr>]

-------- Original Message -------- Subject: SMT 2013 Call For Papers Date: Thu, 21 Mar 2013 18:28:04 +0100 From: Roberto Bruttomesso <roberto.bruttomesso AT gmail.com> To: Alberto Griggio <griggio AT fbk.eu>

[**** We apologize if you receive multiple copies of this message ****]

======================================================================

SMT Workshop 2013

11th International Workshop on Satisfiability Modulo Theories

Affiliated with SAT 2013, Helsinki, Finland

July 8th - 9th, 2013

http://smt2013.fbk.eu

--- 2nd CALL FOR PAPERS ---

======================================================================

Background

----------

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,

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 aim of the workshop is to bring together researchers and users of

SMT tools and techniques. Relevant topics 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 14th, 2013

* Notification - May 12th, 2013

* Camera ready versions due - May 19th, 2013

* Workshop - July 8th and 9th, 2013

Paper submission and Proceedings

--------------------------------

Three categories of submissions are invited:

* Extended abstracts: given the informal style of the workshop, 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 they 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

available.

* Presentation-only papers: describe work recently published or

submitted and will not be included in the proceedings. We see this

as a way to provide additional access to important developments that

SMT Workshop attendees may be unaware of.

Papers in all three categories will be peer-reviewed. Papers should

not exceed 10 pages (Postscript or PDF) and should be in

standard-conforming Postscript or PDF. Technical details may be

included in an appendix to be read at the reviewers' discretion.

Final versions should be prepared in LaTeX using the easychair.cls

class file.

To submit a paper, go to the EasyChair SMT page

http://www.easychair.org/conferences/?conf=smt2013 and follow the

instructions there.

Program Committee

-----------------

* Roberto Bruttomesso (Atrenta), co-chair

* Morgan Deters (New York University)

* Bruno Dutertre (SRI)

* Pascal Fontaine (Loria, INRIA, University of Nancy)

* Malay Ganai (NEC Labs America)

* Alberto Griggio (FBK), co-chair

* Sava Krstic (Intel Corporation)

* Zvonimir Rakamaric (University of Utah)

* Silvio Ranise (FBK)

* Philipp Ruemmer (Uppsala University)

* Ofer Strichman (Technion)

* Cesare Tinelli (The University of Iowa)

* Christoph M. Wintersteiger (Microsoft Research)

Invited Speakers

----------------

Sylvain Conchon Université Paris-Sud

Thomas Sturm            Max-Planck-Institut für Informatik