• SYMBA

• Referenced in 13 articles [sw08528]
• functions in the theory of linear real arithmetic (LRA). Given a formula...

• SMT-RAT

• Referenced in 19 articles [sw13091]
• solving quantifier-free (non)linear real and integer arithmetic (QF_LRA...

• MiniSat

• Referenced in 584 articles [sw00577]
• An extensible SAT-solver. MiniSat is a minimalistic...

• Yices

• Referenced in 157 articles [sw04436]
• Yices is an efficient SMT solver that decides...

• z3

• Referenced in 606 articles [sw04887]
• Z3 is a high-performance theorem prover being...

• dReal

• Referenced in 34 articles [sw07157]
• dReal: an SMT solver for nonlinear theories over...

• CalCS

• Referenced in 8 articles [sw13098]
• CalCS: SMT solving for non-linear convex constraints...

• nuXmv

• Referenced in 28 articles [sw18526]
• The nuXmv Symbolic Model Checker. This paper describes...

• Spacer

• Referenced in 12 articles [sw19496]
• SMT-based model checking for recursive programs. We...

• PySMT

• Referenced in 5 articles [sw19843]
• PySMT: a solver-agnostic library for fast prototyping...

• HYST

• Referenced in 8 articles [sw20137]
• HyST: A Source Transformation and Translation Tool for...

• HyComp

• Referenced in 4 articles [sw20163]
• HyComp: An SMT-based model checker for hybrid...

• dReach

• Referenced in 19 articles [sw20164]
• dReach:(δ)-reachability analysis for hybrid systems. dReach...

• CTIGAR

• Referenced in 9 articles [sw23310]
• Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR). Typical...

• iSAT

• Referenced in 4 articles [sw28679]
• Recent improvements in the SMT solver iSAT. Over...