Preface to Special Issue on Satisfiability Modulo Theories

Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of first-order formulae with respect to some decidable background theory (e.g., linear arithmetic, the theory of arrays, the theory of bit-vectors). SMT techniques are gaining increasing relevance in many application domains, including formal verification of hardware and software, compiler optimization, planning and scheduling. SMT is strongly related to SAT, as most SMT tools are built on top of or interface with efficient SAT solvers. This special issue includes four papers selected from the six submissions sent in response to an open call for papers. As a part of the selection process we solicited three reviews for each paper. We would like to thank the anonymous reviewers for their work, the authors for their contributions, and Hans van Maaren for the opportunity to publish this special issue.