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 |
---|
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 |
---|
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 |
---|
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 |
---|