| 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 |
|---|
| clipper2 | Polygon Clipping and Offsetting |
|---|
| cliquer | C routines for finding cliques in an arbitrary weighted graph |
|---|
| coq | Coq/Rocq is a 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 |
|---|
| coq-stdlib | Stdlib for the Coq/Rocq Prover, used to be part of Coq |
|---|
| 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 |
|---|
| manifold | Geometry library for topological robustness |
|---|
| mathematica | Wolfram Mathematica |
|---|
| 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 |
|---|
Packages