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.
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)
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 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
- Submission deadline: April 14th, 2013 EXTENDED until April 22nd, 2013
- Notification: May 12th, 2013 May 20th, 2013
- Camera ready versions due: May 19th, 2013 May 27th, 2013
- Workshop: July 8th and 9th, 2013
- Registration deadlines:
- Early: May 27
- Late: June 21
Registration
SAT 2013 registration is now open at http://sat2013.cs.helsinki.fi/registration.html
Some accommodation options are listed at http://sat2013.cs.helsinki.fi/accommodation.html We encourage to also check alternative options and prices. Remember to also book your accommodation early.
For local information, see http://sat2013.cs.helsinki.fi/local.html
Proceedings
Only informal proceedings will be distributed at the workshop.Program
The workshop will have two invited speakers:- Sylvain Conchon, LRI, Université Paris-Sud
- Thomas Sturm, Max-Planck-Institut für Informatik, Saarbrücken
1st Day (Monday July 8th)
| Registration | |
| 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) |
| Break | |
| 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) |
| Lunch | 14.00 - 15.00 | Invited Talk 1: Thomas Sturm (MPI Saarbruecken) Effective Quantifier Elimination and Decision - Theory, Implementations, Applications, Perspectives |
| Break | |
| 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) |
| Break | |
| 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