4ti2 | Software package for algebraic, geometric and combinatorial problems |
---|
abc | System for sequential logic synthesis and formal verification |
---|
acl2 | Industrial strength theorem prover, logic and programming language |
---|
alectryon | Toolkit for literate programming in Coq |
---|
alt-ergo | Automatic theorem prover |
---|
arb | C library for arbitrary-precision interval arithmetic |
---|
bertini | Software for Numerical Algebraic Geometry |
---|
boolector | Fast SMT solver for bit-vectors, arrays and uninterpreted functions |
---|
btor2tools | Generic parser and tools for the BTOR2 format |
---|
cadabra | Field-theory motivated approach to computer algebra |
---|
cadical | Simplified Satisfiability Solver |
---|
calc | Arbitrary precision C-like arithmetic system |
---|
cgal | C++ library for geometric algorithms and data structures |
---|
cliquer | C routines for finding cliques in an arbitrary weighted graph |
---|
coq | Proof assistant written in O'Caml |
---|
coq-mathcomp | Mathematical Components for the Coq proof assistant |
---|
coq-serapi | Serialization library and protocol for interaction with the Coq proof assistant |
---|
cryptominisat | Advanced SAT solver with C++ and command-line interfaces |
---|
cubicle | Model checker for verifying properties of array-based systems |
---|
cudd | Colorado University binary Decision Diagram library |
---|
cvc4 | Automatic theorem prover for satisfiability modulo theories (SMT) problems |
---|
dataplot | Program for scientific visualization and statistical analyis |
---|
diagrtb | Calculation of some eigenvectors of a large real, symmetrical, matrix |
---|
dsfmt | Double precision SIMD-oriented Fast Mersenne Twister library |
---|
dunshire | Python library to solve linear games over symmetric cones |
---|
easycrypt | Computer-Aided Cryptographic Proofs |
---|
eclib | Programs for elliptic curves defined over the rational numbers |
---|
ent | Random number sequence test and entropy calculation |
---|
eprover | Automated theorem prover for full first-order logic with equality |
---|
euler | Mathematical programming environment |
---|
fann | Fast Artificial Neural Network Library |
---|
flint | Fast Library for Number Theory |
---|
flocq | Formalization of floating-point arithmetic for the Coq proof assistant |
---|
form | Symbolic Manipulation System |
---|
fricas | FriCAS is a fork of Axiom computer algebra system |
---|
frobby | Software system and project for computations with monomial ideals |
---|
gap | System for computational discrete algebra. Core functionality. |
---|
gappa | Tool for verifying floating-point or fixed-point arithmetic |
---|
gappalib-coq | Allows the certificates Gappa generates to be imported by the Coq |
---|
genius | Genius Mathematics Tool and the GEL Language |
---|
geogebra-bin | Mathematics software for geometry |
---|
geomview | Interactive Geometry Viewer |
---|
gfan | Compute Groebner fans and tropical varieties |
---|
giac | A free C++ Computer Algebra System library and its interfaces |
---|
gimps | The Great Internet Mersenne Prime Search |
---|
ginac | C++ library and tools for symbolic calculations |
---|
glpk | GNU Linear Programming Kit |
---|
gmm | Generic C++ template library for sparse, dense and skyline matrices |
---|
gmp-ecm | Elliptic Curve Method for Integer Factorization |
---|
gp2c | A GP to C translator |
---|
gretl | Regression, econometrics and time-series library |
---|
gsl-shell | Lua interactive shell for sci-libs/gsl |
---|
jags | Just Another Gibbs Sampler for Bayesian MCMC simulation |
---|
kind2 | Multi-engine SMT-based automatic model checker |
---|
kissat | Keep-it-simple and clean bare metal SAT solver written in C |
---|
lcalc | Command-line utility and library for L-function computations |
---|
lean | The Lean Theorem Prover |
---|
libpoly | C library for manipulating polynomials |
---|
lpsolve | Mixed Integer Linear Programming (MILP) solver |
---|
lrcalc | Littlewood-Richardson Calculator |
---|
mathematica | Wolfram Mathematica |
---|
mathlib-tools | Development tools for Lean's mathlib |
---|
mathmod | Plot parametric and implicit surfaces |
---|
mathomatic | Automatic algebraic manipulator |
---|
maxima | Free computer algebra environment based on Macsyma |
---|
metamath | Proof verifier based on a minimalistic formalism |
---|
metamath-databases | Sample databases for Metamath |
---|
minisat | Small yet efficient SAT solver with reference paper |
---|
msieve | A C library implementing a suite of algorithms to factor large integers |
---|
nauty | Computing automorphism groups of graphs and digraphs |
---|
nestedsums | A GiNaC-based library for symbolic expansion of certain transcendental functions |
---|
normaliz | Tool for computations in affine monoids and more |
---|
num-utils | A set of programs for dealing with numbers from the command line |
---|
octave | High-level interactive language for numerical computations |
---|
octave-epstk | Graphical output functions for Matlab and Octave |
---|
opensmt | Compact and open-source SMT-solver written in C++ |
---|
otter | An Automated Deduction System |
---|
palp | A Package for Analyzing Lattice Polytopes (PALP) |
---|
pari | Computer-aided number theory C library and tools |
---|
pari-data | Additional dataset packages for PARI |
---|
petsc | Portable, Extensible Toolkit for Scientific Computation |
---|
picosat | SAT solver with proof and core support |
---|
planarity | The edge addition planarity suite of graph algorithms |
---|
plfit | Fit power-law distributions to empirical data |
---|
polymake | Tool for polyhedral geometry and combinatorics |
---|
primecount | Highly optimized CLI and library to count primes |
---|
primesieve | CLI and library for quickly generating prime numbers |
---|
prng | Pseudo-Random Number Generator library |
---|
prover9 | Automated theorem prover for first-order and equational logic |
---|
proverif | Cryptographic protocol verifier in the formal model |
---|
psmt2-frontend | Library to parse and type-check an extension of the SMT-LIB 2 standard |
---|
pspp | Program for statistical analysis of sampled data |
---|
rkward | IDE for the R-project |
---|
rngstreams | Multiple independent streams of pseudo-random numbers |
---|
rw | Compute rank-width decompositions of graphs |
---|
sha1-polyml | implementation of SHA1 is taken from the GNU coreutils package |
---|
singular | Computer algebra system for polynomial computations |
---|
slepc | Scalable Library for Eigenvalue Problem Computations |
---|
smtinterpol | Interpolating SMT-solver computing Craig interpolants for various theories |
---|
spin | An efficient logic-model checker for the verification of multi-threaded code |
---|
stp | Simple Theorem Prover, an efficient SMT solver for bitvectors |
---|
sympow | Symmetric power elliptic curve L-functions |
---|
topcom | Computing Triangulations Of Point Configurations and Oriented Matroids |
---|
twelf | Implementation of the logical framework LF |
---|
unuran | Universal Non-Uniform Random number generator |
---|
vampire | The Vampire Prover, theorem prover for first-order logic |
---|
verifpal | Cryptographic protocol analysis for real-world protocols |
---|
verit | An open, trustable and efficient SMT-prover |
---|
why3 | Platform for deductive program verification |
---|
why3-for-spark | Platform for deductive program verification |
---|
wxmaxima | Graphical frontend to Maxima, using the wxWidgets toolkit |
---|
yacas | General purpose computer algebra system |
---|
yafu | Yet another factoring utility |
---|
yices2 | SMT Solver supporting SMT-LIB and Yices specification language |
---|
z3 | An efficient theorem prover |
---|