• z3

  • Referenced in 509 articles [sw04887]
  • real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers...
  • Yices

  • Referenced in 141 articles [sw04436]
  • tuples, records, extensional arrays, fixed-size bit-vectors, quantifiers, and lambda expressions. Yices also does...
  • MathSAT

  • Referenced in 58 articles [sw09449]
  • linear arithmetic, and the theory of bit-vectors. It was explicitly designed for being used...
  • Boolector

  • Referenced in 28 articles [sw00085]
  • Boolector: an efficient SMT solver for bit-vectors and arrays. Satisfiability Modulo Theories ... quantifier-free theories of bit-vectors and arrays. It uses term rewriting, bit-blasting ... handle bit-vectors, and lemmas on demand for arrays...
  • SatAbs

  • Referenced in 39 articles [sw12804]
  • This includes a sound treatment of bit-vector overflow, and of the ANSI-C pointer...
  • Beaver

  • Referenced in 9 articles [sw00071]
  • Engineering an efficient SMT solver for bit-vector arithmetic. Beaver is an SMT solver (theorem ... theory of quantifier-free finite-precision bit-vector arithmetic. It supports all operators defined under...
  • PASS

  • Referenced in 7 articles [sw21858]
  • interest recently. Existing methods use either bit-vectors or automata (or their combination) to model ... strings, and reduce string constraints to bit-vector constraints or automaton operations, which are then ... need to enumerate string lengths (as bit-vector based methods do), or concrete string values...
  • bv2epr

  • Referenced in 7 articles [sw07142]
  • tool for polynomially translating quantifier-free bit-vector formulas into EPR Bit-precise reasoning ... efficient approaches for solving fixed-size bit-vector formulas have been developed. Most of these ... then showed that solving quantifier-free bit-vector formulas (QF_BV) is NExpTime-complete...
  • OptiMathSAT

  • Referenced in 7 articles [sw32308]
  • equality and uninterpreted functions, linear arithmetic, bit-vectors, arrays). Like MathSAT 5, OptiMathSAT...
  • URBiVA

  • Referenced in 3 articles [sw09448]
  • URBiVA: uniform reduction to bit-vector arithmetic. We describe a system URBiVA for specifying ... problems by uniformly reducing them to bit-vector arithmetic (bva). A problem description is given...
  • RazerS

  • Referenced in 4 articles [sw22766]
  • faster, banded version of the Myers’ bit-vector algorithm for verification, memory-saving measures...
  • SCOOT

  • Referenced in 3 articles [sw09954]
  • support for concurrency and arbitrary-width bit-vector arithmetic. The existing static analyzers for SystemC...
  • Smacc

  • Referenced in 2 articles [sw14305]
  • approximations. SmacC uses the logic for bit-vectors with arrays to construct a bit-precise...
  • SONOLAR

  • Referenced in 2 articles [sw26291]
  • that solves quantifier-free fixed-size bit-vector logic formulas. The solver supports...
  • BSIFT

  • Referenced in 1 article [sw28343]
  • scale image retrieval applications. Feature quantization by vector quantization plays a crucial role ... descriptor to a descriptive and discriminative bit-vector, which is called binary SIFT (BSIFT...
  • UppSAT

  • Referenced in 1 article [sw26289]
  • arithmetic (encoded into the theory of bit-vectors in practice). In an experimental evaluation...
  • FLAME

  • Referenced in 1 article [sw36879]
  • queries and the second uses bit-vector techniques. The algorithm starts by constructing matches...
  • Vaquita

  • Referenced in 1 article [sw33127]
  • selected regions using a fast bit-vector algorithm. Furthermore, it also considers the discrepancy...
  • MiniSat

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

  • Referenced in 28 articles [sw00766]
  • In this paper we describe QuBE++, an efficient...