SMT 2012: Editor's Preface

This volume contains the papers presented at the tenth edition of the International Workshop on Satisfiability Modulo Theories (SMT-2012). The workshop was held on June 30 and July~1, 2012, in Manchester, UK, in association with the Sixth International Joint Conference on Automated Reasoning (IJCAR-2012), as part of the Alan Turing Year 2012, held just after The Alan Turing Centenary Conference.

After ten years of this series of workshops, the SMT paradigm for determining the satisfiability of first-order formulas modulo background theories is still developing fast, and interest in SMT solving is increasing, probably faster than ever. The SMT Workshop is certainly the main annual event of the community, where both researchers and users of SMT technology can meet and discuss new theoretical ideas, implementation and evaluation techniques, and applications.

In order to facilitate more exploration and increased discussion of newer ideas, this year we invited submissions in three categories:

• extended abstracts, to present preliminary reports of work in progress;
• original papers, to describe original and mature research (simultaneous submissions were not allowed);
• presentation-only papers, to provide additional access to important developments that SMT Workshop attendees may be unaware of. These works may have been recently published or submitted.

Papers were solicited on topics that include all aspects of Satisfiability Modulo Theory solving. More specifically, some suggested topics were:

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

We received thirteen papers. Each submission was reviewed by three program committee members. Due to the quality of and interest in the submissions, and in keeping with the desire to encourage presentation and discussion of works in progress, we were able to accept all contributions for presentation at the workshop. The program included one presentation only: Invariant discovery by efficient sifting by Temesghen Kahsai, Yeting Ge and Cesare Tinelli.

We would like to thank the following people and organizations for helping to make SMT a success:

• the authors and participants of the workshop;
• the invited speakers;
• the program committee and the reviewers for their work;
• the organizers of the PAAR workshop, for the organization of the joint SMT-PAAR invited talk;
• our sponsors, Microsoft and Intel.

We are very grateful to the IJCAR organizers for their support and for hosting the workshop, and are indebted to the EasyChair team for the availability of the EasyChair Conference System.