• Boogie

  • Referenced in 118 articles [sw07714]
  • conditions that are passed to an SMT solver. The default SMT solver...
  • Yices

  • Referenced in 141 articles [sw04436]
  • Yices is an efficient SMT solver that decides the satisfiability of arbitrary formulas containing uninterpreted...
  • VeriFast

  • Referenced in 57 articles [sw07705]
  • about the primitive recursive functions. An SMT solver is used to solve queries over data ... that prevents non-termination of the SMT solver while enabling reduction of any ground term ... either the verifier or the SMT solver, verification time is predictable...
  • MathSAT

  • Referenced in 58 articles [sw09449]
  • MathSAT 4 SMT Solver. We present MathSAT 4, a state-of-the-art SMT solver ... provides functionalities which extend the applicability of SMT in this setting. In particular: model generation...
  • MathSAT5

  • Referenced in 45 articles [sw09569]
  • mathsat5 SMT solver. MathSAT is a long-term project, which has been jointly carried ... maintaining a state-of-the-art SMT tool for formal verification (and other applications). MathSAT5 ... SMT formulae; finally, a framework allowing users for plugging their custom tuned SAT solvers. MathSAT5...
  • veriT

  • Referenced in 30 articles [sw07281]
  • veriT: An Open, Trustable and Efficient SMT-Solver. This article describes the first public version ... satisfiability modulo theory (SMT) solver veriT. It is open-source, proof-producing, and complete...
  • Boolector

  • Referenced in 28 articles [sw00085]
  • Boolector: an efficient SMT solver for bit-vectors and arrays. Satisfiability Modulo Theories ... Boolector, which is an efficient SMT solver for the quantifier-free theories of bit-vectors...
  • dReal

  • Referenced in 28 articles [sw07157]
  • Dreal: an SMT solver for nonlinear theories over the reals We describe the open-source ... tool dReal, an SMT solver for nonlinear formulas over the reals. The tool can handle...
  • OpenSMT

  • Referenced in 28 articles [sw08426]
  • incremental, efficient, and open-source SMT-solver. OpenSMT has been specifically designed to be easily...
  • EasyCrypt

  • Referenced in 29 articles [sw09738]
  • checked automatically using off-the-shelf SMT solvers and automated theorem provers, and then compiled...
  • SMT-RAT

  • Referenced in 18 articles [sw13091]
  • combined to (1) an SMT solver or (2) a theory solver in order to extend ... supported logics of an existing SMT solver by the supported logics of SMT-RAT. Further...
  • SYMBA

  • Referenced in 11 articles [sw08528]
  • Symbolic optimization with SMT solvers. The rise in efficiency of Satisfiability Modulo Theories (SMT) solvers ... these applications, SMT solvers are used for generating satisfying assignments (e.g., a witness ... calls. Unfortunately, none of the available SMT solvers offer such optimization capabilities. In this paper ... value of t. SYMBA utilizes efficient SMT solvers as black boxes. As a result...
  • SMTInterpol

  • Referenced in 20 articles [sw07406]
  • SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories. The solver...
  • WoLFram

  • Referenced in 15 articles [sw02075]
  • software. It is shown, that modern SAT solvers can formally verify PLC programs within ... Boolean SAT engine with an SMT solver is an option to cope with the complexity...
  • vZ

  • Referenced in 10 articles [sw22666]
  • Optimizing SMT Solver. νZ is a part of the SMT solver Z3. It allows users ... approaches for solving linear optimization problems over SMT formulas, MaxSMT, and their combinations. Objective functions ... that allows dispatching problems to special purpose solvers, and examine use cases...
  • LLBMC

  • Referenced in 15 articles [sw09478]
  • bounded model checking using an SMT solver and thus achieves bit-accurate precision. A distinguishing...
  • Beaver

  • Referenced in 9 articles [sw00071]
  • Beaver: Engineering an efficient SMT solver for bit-vector arithmetic. Beaver is an SMT solver ... operators. Beaver is specially adapted for solving SMT formulae arising out of program analysis (rich...
  • dReach

  • Referenced in 13 articles [sw20164]
  • delta-decision procedures in the SMT solver dReach. In this way, dReach is able...
  • ESBMC

  • Referenced in 7 articles [sw09946]
  • software based on Satisfiability Modulo Theories (SMT) solver. It allows the verification engineer ... passes them directly to an SMT solver. In addition, ESBMC can output verification conditions using ... CProver framework. ESBMC uses the SMT solvers Z3 (default) and Boolector, which are also included...
  • Norn

  • Referenced in 6 articles [sw21853]
  • Norn: an SMT solver for string constraints. We present version 1.0 of the Norn ... SMT solver for string constraints. Norn is a solver for an expressive constraint language, including ... feature distinguishing Norn from other SMT solvers, Norn is a decision procedure under the assumption...