• SMT-LIB

  • Referenced in 187 articles [sw04103]
  • SMT-LIB was created with the expectation that the availability of common standards ... facilitate the evaluation and the comparison of SMT systems, and advance the state...
  • CVC4

  • Referenced in 109 articles [sw09485]
  • automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove ... support the features of CVC3 and SMT-LIBv2 while optimizing the design of the core ... intended to be an open and extensible SMT engine, and it can be used...
  • Boogie

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

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

  • Referenced in 85 articles [sw04886]
  • automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. CVC3 is the last offspring ... series of popular SMT provers, which originated at Stanford University with the SVC system...
  • 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...
  • VeriFast

  • Referenced in 57 articles [sw07705]
  • facts about the primitive recursive functions. An SMT solver is used to solve queries over ... described that prevents non-termination of the SMT solver while enabling reduction of any ground ... performed by either the verifier or the SMT solver, verification time is predictable...
  • 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 ... tool. It supports most of the SMT-LIB theories and their combinations, and provides many ... improved incrementality support, which is vital in SMT applications; second, a full support...
  • Boolector

  • Referenced in 28 articles [sw00085]
  • Boolector: an efficient SMT solver for bit-vectors and arrays. Satisfiability Modulo Theories ... SMT) is the problem of deciding satisfiability of a logical formula, expressed in a combination ... features of Boolector, which is an efficient SMT solver for the quantifier-free theories...
  • 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...
  • dReal

  • Referenced in 29 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...
  • SMT-RAT

  • Referenced in 18 articles [sw13091]
  • SMT-RAT is an open source C++ toolbox for strategic and parallel SMT solving consisting ... collection of SMT compliant implementations of methods for solving quantifier-free (non)linear real ... modules can be combined to (1) an SMT solver or (2) a theory solver ... extend the supported logics of an existing SMT solver by the supported logics...
  • Clingcon

  • Referenced in 34 articles [sw09892]
  • adopts state-of-the-art techniques from SMT and uses conflict-driven learning and theory...
  • Mcmt

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

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

  • Referenced in 20 articles [sw27563]
  • puts together the automation of an SMT-backed deductive verification tool with the expressive power ... meet their specifications using a combination of SMT solving and interactive proofs...
  • OpenSMT

  • Referenced in 28 articles [sw08426]
  • OpenSMT, an incremental, efficient, and open-source SMT-solver. OpenSMT has been specifically designed...
  • nuXmv

  • Referenced in 25 articles [sw18526]
  • Integers and Reals, and it provides advanced SMT-based model checking techniques. Besides extended functionalities...
  • Moses

  • Referenced in 24 articles [sw10650]
  • language models. In addition to the SMT decoder, the toolkit also includes a wide variety...
  • smt

  • Referenced in 14 articles [sw09205]
  • smt: A Matlab toolbox for structured matrices. The full exploitation of the structure of large ... arithmetic operators and functions on them. The smt toolbox for Matlab introduces two new classes...