SMT Workshop 2013

11th International Workshop on Satisfiability Modulo Theories

Affiliated with the 16th International Conference on Theory and Applications of Satisfiability Testing
(SAT 2013)

July 8th, 9th, 2013

Helsinki, Finland


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:

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

Program committee

Paper submission and Proceedings

Informal Proceedings.

Call For Papers.

Three categories of submissions are invited:

Papers in all three categories are 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 and follow the instructions there.

Important dates


SAT 2013 registration is now open at

Some accommodation options are listed at We encourage to also check alternative options and prices. Remember to also book your accommodation early.

For local information, see


Only informal proceedings will be distributed at the workshop.


The workshop will have two invited speakers:

1st Day (Monday July 8th)

Session 1: Bit-Vectors and Arrays
09.00 - 09.30 Andreas Froehlich, Gergely Kovasznai and Armin Biere
Efficiently Solving Bit-Vector Problems Using Model Checkers (Slides)
09.30 - 10.00 Alexander Nadel
Handling Bit-Propagating Operations in Bit-Vector Reasoning (Slides)
10.00 - 10.30 Stephan Falke, Florian Merz and Carsten Sinz
Extending the Theory of Arrays: memset, memcpy and Beyond (Slides)
Session 2: Applications
11.00 - 11.30 Ian Blumenfeld, Roberta Faux, Paul Li and Mark Raugas
SMT Solvers for Malware Unpacking (Slides)
11.30 - 12.00 Boyan Yordanov, Christoph M. Wintersteiger, Youssef Hamadi and Hillel Kugler
Z34Bio: A Framework for Analyzing Biological Computation (Slides)
12.00 - 12.30 Andrew Mihal
A Difference Logic Formulation and SMT Solver for Timing-Driven Placement (Slides)
14.00 - 15.00 Invited Talk 1: Thomas Sturm (MPI Saarbruecken)
Effective Quantifier Elimination and Decision - Theory, Implementations, Applications, Perspectives
Session 3: Proofs
15.30 - 16.00 Bruno Woltzenlogel Paleo and Joseph Boudou
Compression of Propositional Resolution Proofs by Lowering Subproofs (Slides)
16.00 - 16.30 Juergen Christ and Jochen Hoenicke
Extending Proof Tree Preserving Interpolation to Sequences and Trees (Slides)
SMT-LIB, SMT-EVAL and Business Meeting

2nd Day (Tuesday July 9th)

09.00 - 10.00 Invited Talk 2: Sylvain Conchon (Universitè Paris-Sud)
Cubicle: Design and Implementation of an SMT based Model Checker for Parameterized Systems
Session 4: Quantifiers
10.00 - 10.30 Andrew Reynolds, Cesare Tinelli, Amit Goel and Sava Krstic
Finite Model Finding in SMT (Slides)
11.00 - 11.30 Aboubakr Achraf El Ghazi, Mana Taghdiri, Mattias Ulbrich and Mihai Herda
Reducing the Complexity of Quantified Formulas via Variable Elimination (Slides)
Session 5: Tools
11.30 - 12.00 Carlos Areces, David Deharbe, Pascal Fontaine and Ezequiel Orbe
SyMT: finding symmetries in SMT formulas (Slides)
12.00 - 12.30 Aina Niemetz and Armin Biere
ddSMT: A Delta Debugger for the SMT-LIB v2 Format (Slides)
Concluding Remarks

Previous editions

More information about the SMT workshop series can be found on The International Workshop on Satisfiability Modulo Theories Website
SMT 2012, Manchester, UK - affiliated with IJCAR 2012
SMT 2011, Snowbird, USA - affiliated with CAV 2011
SMT 2010, Edinburgh, UK - affiliated with CAV 2010 and SAT 2010
SMT 2009, Montreal, Canada - affiliated with CADE-22
SMT 2008, Princeton, USA - affiliated with CAV 2008
SMT 2007, Berlin, Germany - affiliated with CAV 2007
PDPAR 2006, Seattle, USA - affiliated with IJCAR 2006
PDPAR 2005, Edinburgh, UK - affiliated with CAV 2005
PDPAR 2004, Cork, Ireland - affiliated with IJCAR 2004
PDPAR 2003, Miami, USA - affiliated with CADE-19