• vZ

  • Referenced in 14 articles [sw22666]
  • Optimizing SMT Solver. νZ is a part of the SMT solver Z3. It allows users ... solve optimization problems modulo theories. Many SMT applications use models to provide satisfying assignments ... approaches for solving linear optimization problems over SMT formulas, MaxSMT, and their combinations. Objective functions...
  • 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...
  • SMTInterpol

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

  • Referenced in 15 articles [sw39472]
  • training data for statistical machine translation (SMT). We trained SMT systems for 110 language pairs...
  • Reluplex

  • Referenced in 20 articles [sw31367]
  • Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. Deep neural networks have emerged...
  • Spacer

  • Referenced in 12 articles [sw19496]
  • SMT-based model checking for recursive programs. We present an SMT-based symbolic model checking ... modular and analyzes procedures individually. Unlike other SMT-based approaches, it maintains both over...
  • SPASS+T

  • Referenced in 19 articles [sw04613]
  • reasoning capabilities of SPASS using an arbitrary SMT procedure for arithmetic and free function symbols...
  • dReach

  • Referenced in 19 articles [sw20164]
  • solved by delta-decision procedures in the SMT solver dReach. In this way, dReach...
  • Cubicle

  • Referenced in 17 articles [sw13778]
  • Cubicle: a parallel smt-based model checker for parameterized systems. Cubicle is a new model...
  • Beaver

  • Referenced in 10 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...
  • Norn

  • Referenced in 10 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...
  • LLBMC

  • Referenced in 16 articles [sw09478]
  • based on bounded model checking using an SMT solver and thus achieves bit-accurate precision...
  • WoLFram

  • Referenced in 15 articles [sw02075]
  • Replacing the Boolean SAT engine with an SMT solver is an option to cope with...
  • BarcelogicTools

  • Referenced in 9 articles [sw02001]
  • Barcelogic for SMT is an efficient implementation of the DPLL(T) framework [Ganzingeretal2004CAV, Nieuwenhuisetal2005LPAR ... simple interface [Ganzingeretal2004CAV]. Currently, Barcelogic for SMT supports difference logic over the integers ... system have to be in the SMT-LIB format...
  • ESBMC

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

  • Referenced in 14 articles [sw38338]
  • based on nested lazy model enumeration through SMT-solving, and projections. This scheme...
  • raSAT

  • Referenced in 8 articles [sw15206]
  • raSAT: SMT solver for Polynomial Constraints on Real numbers. raSAT is an SMT to solve ... linux. raSAT accepts inequality problems in SMT-LIB format (.smt2) (including...
  • PROPhESY

  • Referenced in 13 articles [sw33602]
  • PROPhESY supports incremental automatic parameter synthesis (using SMT techniques) to determine “safe” and “unsafe” regions...
  • SMTCoq

  • Referenced in 7 articles [sw32310]
  • SMTCoq: a plug-in for integrating smt solvers into Coq. This paper describes SMTCoq ... check answers from external SAT and SMT solvers and to increase Coq’s automation using ... solver ZChaff, for propositional logic, and the SMT solvers veriT and CVC4, for the quantifier...
  • CalCS

  • Referenced in 8 articles [sw13098]
  • CalCS: SMT solving for non-linear convex constraints. Certain formal verification tasks require reasoning about ... programming to realize a satisfiability modulo theory (SMT) solver. Our solver, CalCS, uses a lazy...