Satisfiable Modulo Theories Solver (SMT Solver)
Satisfiable Modulo Theories (SMT) Solvers are software tools for the efficient and fully automatic analysis of the satisfiability of a formula in predicate logic with theories.
Examples of SMT Solvers:
- CVC4 (https://cvc4.github.io)
- Yices (https://yices.csl.sri.com)
- Z3 (https://github.com/Z3Prover/z3)
Examples of their applications:
- Program verification
- Analysis of requirements models
- Microprocessor verification