Summary
Satisfiability Modulo Theories (SMT) problems are akin to mathematical puzzles: given a mix of equations and logical rules, an SMT solver determines whether there exists an assignment of variables that satisfies everything at once. SMT solving underpins high-stakes assurance tasks: for example, proving that a self-driving car cannot steer into an obstacle under modeled operating conditions, and supporting safety checks in domains like avionics, medical devices, and power systems. These problems become increasingly challenging as modern software and systems incorporate machine learning (ML) and
