SMT: Something You Must Try

SMT (Satisfiability Modulo Theories) solving is a technology for the fully automated solution of logical formulas. Due to their impressive efficiency, SMT solvers are nowadays frequently used in a wide variety of applications. These tools are general purpose and as off-the-shelf solvers, their usage is truly integrated. A typical application (i) encodes real-world problems as logical formulas, (ii) check these formulas for satisfiability with the help of SMT solvers, and - in case of satisfiability - (iii) decodes their solutions back to solutions of the original real-world problem. In this extended abstract we give some insights into the working mechanisms of SMT solving, discuss a few areas of application, and present a novel application from the domain of simulation.