
z3
 Referenced in 510 articles
[sw04887]
 Microsoft Research.Z3 supports linear real and integer arithmetic, fixedsize bitvectors, extensional arrays, uninterpreted...

REDUCE
 Referenced in 740 articles
[sw00789]
 with symbolic matrices; arbitrary precision integer and real arithmetic; facilities for defining new functions...

Yices
 Referenced in 141 articles
[sw04436]
 symbols with equality, linear real and integer arithmetic, scalar types, recursive datatypes, tuples, records, extensional...

gmp
 Referenced in 272 articles
[sw00363]
 free library for arbitrary precision arithmetic, operating on signed integers, rational numbers, and floating point ... achieved by using fullwords as the basic arithmetic type, by using fast algorithms, with highly...

Why3
 Referenced in 130 articles
[sw04438]
 standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps...

Princess
 Referenced in 25 articles
[sw06872]
 FirstOrder Logic modulo Linear Integer Arithmetic. Princess is a theorem prover for Presburger arithmetic ... Princess can reason about problems in integer arithmetic without multiplication (only multiplication with integer literals...

MIRACL
 Referenced in 29 articles
[sw06009]
 MIRACL (Multiprecision Integer and Rational Arithmetic C/C++ Library). Multiprecision Integer and Rational Arithmetic Cryptographic Library...

SMTRAT
 Referenced in 18 articles
[sw13091]
 quantifierfree (non)linear real and integer arithmetic...

LiDIA
 Referenced in 52 articles
[sw00518]
 contains tools for rational integers and some floating point arithmetic, however. Emphasis...

UCLID
 Referenced in 25 articles
[sw04657]
 theories of uninterpreted functions and equality, integer linear arithmetic, and arrays. UCLID can also handle...

Fermat
 Referenced in 41 articles
[sw00277]
 Fordham University, that does arithmetic of arbitrarily long integers and fractions, multivariate polynomials, symbolic calculations...

Spacer
 Referenced in 11 articles
[sw19496]
 best BDDbased algorithms. For Linear Arithmetic (integers and rationals), we give an efficient instantiation...

ARIBAS
 Referenced in 10 articles
[sw07341]
 interactive interpreter for big integer arithmetic and multiprecision floating point arithmetic with a Pascal/Modula...

PANDA
 Referenced in 6 articles
[sw12654]
 option of doing computations in exact integer arithmetic, the exploitation of symmetry information...

SIMPLY
 Referenced in 5 articles
[sw11807]
 falling into the quantifier free linear integer arithmetic logic. The compiler has been developed with...

CpGcluster
 Referenced in 4 articles
[sw35410]
 bulk genome. Conclusion: CpGcluster uses only integer arithmetic, thus being a fast and computationally efficient...

lrslib
 Referenced in 3 articles
[sw37045]
 comes with a choice of three arithmetic packages. Input file formats are compatible with Komei ... either multiple precision or fixed integer arithmetic. Output is not stored in memory, so even...

SMTCoq
 Referenced in 3 articles
[sw32310]
 vectors, functional arrays with extensionality, linear integer arithmetic, and uninterpreted function symbols...

LIRA
 Referenced in 7 articles
[sw21270]
 LIRA: Handling constraints of linear arithmetics over the integers and the reals. The mechanization ... techniques for firstorder logics with linear arithmetic, namely...

Salsa
 Referenced in 5 articles
[sw25430]
 algorithms and a constraint solver for integer linear arithmetic, for discharging the verification conditions...