
z3
 Referenced in 509 articles
[sw04887]
 real and integer arithmetic, fixedsize bitvectors, extensional arrays, uninterpreted functions, and quantifiers...

Yices
 Referenced in 141 articles
[sw04436]
 tuples, records, extensional arrays, fixedsize bitvectors, quantifiers, and lambda expressions. Yices also does...

MathSAT
 Referenced in 58 articles
[sw09449]
 linear arithmetic, and the theory of bitvectors. It was explicitly designed for being used...

Boolector
 Referenced in 28 articles
[sw00085]
 Boolector: an efficient SMT solver for bitvectors and arrays. Satisfiability Modulo Theories ... quantifierfree theories of bitvectors and arrays. It uses term rewriting, bitblasting ... handle bitvectors, and lemmas on demand for arrays...

SatAbs
 Referenced in 39 articles
[sw12804]
 This includes a sound treatment of bitvector overflow, and of the ANSIC pointer...

Beaver
 Referenced in 9 articles
[sw00071]
 Engineering an efficient SMT solver for bitvector arithmetic. Beaver is an SMT solver (theorem ... theory of quantifierfree finiteprecision bitvector arithmetic. It supports all operators defined under...

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

bv2epr
 Referenced in 7 articles
[sw07142]
 tool for polynomially translating quantifierfree bitvector formulas into EPR Bitprecise reasoning ... efficient approaches for solving fixedsize bitvector formulas have been developed. Most of these ... then showed that solving quantifierfree bitvector formulas (QF_BV) is NExpTimecomplete...

OptiMathSAT
 Referenced in 7 articles
[sw32308]
 equality and uninterpreted functions, linear arithmetic, bitvectors, arrays). Like MathSAT 5, OptiMathSAT...

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

RazerS
 Referenced in 4 articles
[sw22766]
 faster, banded version of the Myers’ bitvector algorithm for verification, memorysaving measures...

SCOOT
 Referenced in 3 articles
[sw09954]
 support for concurrency and arbitrarywidth bitvector arithmetic. The existing static analyzers for SystemC...

Smacc
 Referenced in 2 articles
[sw14305]
 approximations. SmacC uses the logic for bitvectors with arrays to construct a bitprecise...

SONOLAR
 Referenced in 2 articles
[sw26291]
 that solves quantifierfree fixedsize bitvector 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 bitvector, which is called binary SIFT (BSIFT...

UppSAT
 Referenced in 1 article
[sw26289]
 arithmetic (encoded into the theory of bitvectors in practice). In an experimental evaluation...

FLAME
 Referenced in 1 article
[sw36879]
 queries and the second uses bitvector techniques. The algorithm starts by constructing matches...

Vaquita
 Referenced in 1 article
[sw33127]
 selected regions using a fast bitvector algorithm. Furthermore, it also considers the discrepancy...

MiniSat
 Referenced in 536 articles
[sw00577]
 An extensible SATsolver. MiniSat is a minimalistic...

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