• z3

  • Referenced in 597 articles [sw04887]
  • developed at Microsoft Research.Z3 supports linear real and integer arithmetic, fixed-size bit-vectors, extensional...
  • INTOPT_90

  • Referenced in 306 articles [sw04705]
  • first chapter (69 pages) introduces interval arithmetic, solving linear interval equations, automatic differentiation and code...
  • NQTHM

  • Referenced in 151 articles [sw07543]
  • integration of a linear arithmetic decision procedure and the addition of a rather primitive facility...
  • FOCI

  • Referenced in 62 articles [sw12868]
  • theories, such as equality, uninterpreted functions, linear arithmetic, and arrays. Most importantly, it can compute...
  • MathSAT

  • Referenced in 61 articles [sw09449]
  • equality and uninterpreted functions, difference logic, linear arithmetic, and the theory of bit-vectors...
  • MUMPS

  • Referenced in 504 articles [sw04013]
  • Solution of large linear systems with symmetric positive definite matrices; general symmetric matrices; general unsymmetric ... matrices; Version for complex arithmetic; Parallel factorization and solve phases (uniprocessor version also available); Iterative...
  • Yices

  • Referenced in 154 articles [sw04436]
  • uninterpreted function symbols with equality, linear real and integer arithmetic, scalar types, recursive datatypes, tuples...
  • BLAS

  • Referenced in 497 articles [sw03216]
  • software packages. Primarily the Fortran BLAS (Basic Linear Algebra Subroutines) collected together by level ... MACHAR software for dynamically determining machine-dependent arithmetic properties...
  • FLINT

  • Referenced in 58 articles [sw00297]
  • including highly optimised routines for polynomial arithmetic and linear algebra in exact rings...
  • INTLAB

  • Referenced in 471 articles [sw04004]
  • inner inclusions and structured matrices) sparse s.p.d. linear systems systems of nonlinear equations (including unconstrained ... univariate polynomial zeros (simple and clusters) interval arithmetic for real and complex data including vectors...
  • CVC

  • Referenced in 49 articles [sw09462]
  • theories of arrays, inductive datatypes, and linear real arithmetic are currently implemented. Other notable features...
  • QOCA

  • Referenced in 30 articles [sw00756]
  • suggested. Currently, QOCA supports linear arithmetic constraints and two different metrics: the square...
  • UCLID

  • Referenced in 25 articles [sw04657]
  • uninterpreted functions and equality, integer linear arithmetic, and arrays. UCLID can also handle limited forms...
  • DERIVE

  • Referenced in 65 articles [sw02964]
  • Problems in the fields of arithmetic, algebra, trigonometry, calculus, linear algebra, and propositional calculus...
  • Princess

  • Referenced in 27 articles [sw06872]
  • Proving in First-Order Logic modulo Linear Integer Arithmetic. Princess is a theorem prover...
  • CSIsat

  • Referenced in 15 articles [sw11407]
  • quantifier-free theory of rational linear arithmetic and equality with uninterpreted function symbols. Our implementation ... combines the efficiency of linear programming for solving the arithmetic part with the efficiency...
  • Alt-Ergo

  • Referenced in 16 articles [sw04888]
  • empty equational theory and by the linear arithmetics. Alt-Ergo contains also a home made...
  • OptiMathSAT

  • Referenced in 11 articles [sw32308]
  • incremental multi-objective optimization over linear arithmetic objective functions, it supports a wide range ... including e.g. equality and uninterpreted functions, linear arithmetic, bit-vectors, arrays). Like MathSAT 5, OptiMathSAT...
  • Mjollnir

  • Referenced in 14 articles [sw38338]
  • certain conditions; we illustrate it for linear real arithmetic. The quantifier elimination problem for linear...
  • InvGen

  • Referenced in 15 articles [sw09780]
  • paper we present InvGen, an automatic linear arithmetic invariant generator for imperative programs. InvGen...