• CVC4

  • Referenced in 109 articles [sw09485]
  • source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used ... prove the validity (or, dually, the satisfiability) of first-order formulas in a large number...
  • cvc3

  • Referenced in 85 articles [sw04886]
  • automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. CVC3 is the last offspring...
  • Boolector

  • Referenced in 28 articles [sw00085]
  • vectors and arrays. Satisfiability Modulo Theories (SMT) is the problem of deciding satisfiability...
  • veriT

  • Referenced in 30 articles [sw07281]
  • first public version of the satisfiability modulo theory (SMT) solver veriT. It is open-source...
  • Mcmt

  • Referenced in 22 articles [sw11911]
  • points by solving Satisfiability Modulo Theories (SMT) problems. Besides standard SMT techniques, efficient heuristics...
  • SYMBA

  • Referenced in 11 articles [sw08528]
  • rise in efficiency of Satisfiability Modulo Theories (SMT) solvers has created numerous uses for them ... these applications, SMT solvers are used for generating satisfying assignments (e.g., a witness...
  • ESBMC

  • Referenced in 7 articles [sw09946]
  • embedded C/C++ software based on Satisfiability Modulo Theories (SMT) solver. It allows the verification engineer...
  • CalCS

  • Referenced in 7 articles [sw13098]
  • CalCS: SMT solving for non-linear convex constraints. Certain formal verification tasks require reasoning about ... paper, we present a new technique for satisfiability solving of Boolean combinations of non-linear ... convex programming to realize a satisfiability modulo theory (SMT) solver. Our solver, CalCS, uses...
  • bv2epr

  • Referenced in 7 articles [sw07142]
  • essential in many applications of satisfiability modulo theories (SMT). In recent years, efficient approaches...
  • LinAIG

  • Referenced in 6 articles [sw10316]
  • exploitation of the capabilities of SMT (Satisfiability Modulo Theories) solvers. Constraint minimization optimizes polyhedra...
  • NLambda

  • Referenced in 5 articles [sw23172]
  • define them, and an external satisfiability modulo theories (SMT) solver is regularly...
  • HyComp

  • Referenced in 4 articles [sw20163]
  • HyComp: An SMT-based model checker for hybrid systems. HyComp is a model checker ... hybrid systems based on Satisfiability Modulo Theories (SMT). HyComp takes as input networks of hybrid...
  • TSAT++

  • Referenced in 3 articles [sw21350]
  • satisfiability modulo theories (SMT). SMT is the problem of determining satisfiability of a propositional combination...
  • Qex

  • Referenced in 3 articles [sw09944]
  • specific background theory for a satisfiability modulo theories (SMT) solver as a set of equational...
  • SMCHR

  • Referenced in 2 articles [sw09322]
  • structure. SMCHR is essentially a satisfiability modulo theories (SMT) solver where the theory...
  • Nopol

  • Referenced in 2 articles [sw26884]
  • into an instance of a Satisfiability Modulo Theory (SMT) problem; then a feasible solution...
  • vZ

  • Referenced in 10 articles [sw22666]
  • optimization problems modulo theories. Many SMT applications use models to provide satisfying assignments...
  • fzn2smt

  • Referenced in 4 articles [sw13501]
  • language version 1.2. SMT stands for Satisfiability Modulo Theories: the problem of deciding the satisfiability ... formula with respect to background theories --such as linear arithmetic, arrays, etc-- for which specialized ... mind of help testing the adequacy of SMT technology outside the field of verification, where...
  • JavaSMT

  • Referenced in 1 article [sw18525]
  • Solvers in Java. Satisfiability Modulo Theory (SMT) solvers received a lot of attention...
  • XSat

  • Referenced in 1 article [sw26290]
  • floating-point satisfiability solver. The Satisfiability Modulo Theory (SMT) problem over floating-point arithmetic ... specify or abstract. State-of-the-art SMT solvers still often run into difficulties when ... This paper proposes a new approach to SMT solving that does not need to directly ... establish the equivalence between floating-point satisfiability and a class of mathematical optimization (MO) problems...