• z3

  • Referenced in 510 articles [sw04887]
  • Microsoft Research.Z3 supports linear real and integer arithmetic, fixed-size bit-vectors, 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]
  • First-Order 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...
  • SMT-RAT

  • Referenced in 18 articles [sw13091]
  • quantifier-free (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 BDD-based 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 multi-precision 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 first-order 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...