4ti2
- Ebuilds: 2, Stable: 1.6.10, Testing: 1.6.10 Description:
4ti2 is a software package for algebraic, geometric and combinatorial problems
on linear spaces and for toric ideals too.
Homepage:https://4ti2.github.io License: GPL-2
abc
- Ebuilds: 2, Testing: 9999 Description:
ABC is a growing software system for synthesis and verification of binary
sequential logic circuits appearing in synchronous hardware designs. ABC
combines scalable logic optimization based on And-Inverter Graphs (AIGs),
optimal-delay DAG-based technology mapping for look-up tables and standard
cells, and innovative algorithms for sequential synthesis and verification.
Homepage:https://people.eecs.berkeley.edu/~alanmi/abc/
https://github.com/berkeley-abc/abc/
acl2
- Ebuilds: 2, Testing: 8.6 Description:
ACL2 is a logic and programming language in which you can model computer
systems, together with a tool to help you prove properties of those models.
"ACL2" denotes "A Computational Logic for Applicative Common Lisp". ACL2 is
part of the Boyer-Moore family of provers, for which its authors have
received the 2005 ACM Software System Award.
Homepage:https://www.cs.utexas.edu/users/moore/acl2/
https://github.com/acl2/acl2/
alectryon
- Ebuilds: 1, Testing: 1.4.0-r2 Description:
A library to process Coq and Lean snippets embedded in text documents,
showing goals and messages for each input sentence. Also a literate
programming toolkit. The goal of Alectryon is to make it easy to write
textbooks, blog posts, and other documents that mix interactive proofs and
prose.
Alectryon originally supported Coq only. Support for Lean is preliminary
and restricted to Lean 3.
Homepage:https://github.com/cpitclaudel/alectryon/
alt-ergo
- Ebuilds: 1, Stable: 2.4.3-r3, Testing: 2.4.3-r3 Description:
Alt-Ergo is an open-source automatic solver of mathematical formulas
designed for program verification. It is based on Satisfiability Modulo
Theories (SMT). Solvers of this family have made impressive advances
and became very popular during the last decade. They are now used is
various domains such as hardware design, software verification and
formal testing.
Homepage:https://alt-ergo.ocamlpro.com
https://github.com/OCamlPro/alt-ergo/
arb
- Ebuilds: 1, Stable: 2.23.0, Testing: 2.23.0 Description:
Arb is a C library for arbitrary-precision interval arithmetic,
using a midpoint-radius representation (“ball arithmetic”). It
supports real and complex numbers, polynomials, power series,
matrices, and evaluation of many transcendental functions. All
operations are done with automatic, rigorous error bounds.
Homepage:https://fredrikj.net/arb/ License: GPL-2+
bertini
- Ebuilds: 1, Testing: 1.6 Description:
Bertini: Software for Numerical Algebraic Geometry
Facts in brief:
Purpose: The numerical solution of systems of polynomial equations
Approach: Homotopy continuation.
Authors: Daniel J. Bates, Jonathan D. Hauenstein, Andrew J. Sommese, Charles W. Wampler
Background: Bertini is a general-purpose solver, written in C, that was
created for research about polynomial continuation.
Homepage:http://bertini.nd.edu License: bertini
cadabra
- Ebuilds: 1, Testing: 2.5.14_p1 Description:
Cadabra is a symbolic computer algebra system (CAS) designed specifically
for the solution of problems encountered in field theory. It has extensive
functionality for tensor computer algebra, tensor polynomial simplification
including multi-term symmetries, fermions and anti-commuting variables,
Clifford algebras and Fierz transformations, component computations,
implicit coordinate dependence, multiple index types and many more.
The input format is a subset of TeX.
Both a command-line and a graphical notebook interface are available, and
you can also use Cadabra from Jupyter by using the Cadabra Jupyter kernel.
Homepage:https://cadabra.science/
https://github.com/kpeeters/cadabra2/
calc
- Ebuilds: 1, Stable: 2.13.0.1, Testing: 2.13.0.1 Description:
Calc is an interactive calculator which provides for easy large
numeric calculations, but which also can be easily programmed for
difficult or long calculations. It can accept a command line argument,
in which case it executes that single command and exits. Otherwise, it
enters interactive mode.
Homepage:http://www.isthe.com/chongo/tech/comp/calc/ License: LGPL-2
cgal
- Ebuilds: 5, Stable: 6.0.1, Testing: 6.1 Description:
The Computational Geometry Algorithms Library is a collaborative
open source library containing:
* the Kernel with geometric primitives such as points, vectors,
lines, predicates for testing things such as relative positions of
points, and operations such as intersections and distance calculation.
* the Basic Library which is a collection of standard data
structures and geometric algorithms, such as convex hull in 2D/3D,
(Delaunay) triangulation in 2D/3D, planar map, polyhedron, smallest
enclosing circle, and multidimensional query structures.
* the Support Library which offers interfaces to other packages,
e.g., for visualisation, and I/O, and other support facilities.
Homepage:https://www.cgal.org/ License: LGPL-3 GPL-3 Boost-1.0
coq
- Ebuilds: 6, Stable: 9.1.0-r1, Testing: 9.1.1, 8.20.0-r1 Description:
Developed in the LogiCal project, the Coq tool is a formal proof
management system: a proof done with Coq is mechanically checked
by the machine.
In particular, Coq allows:
* the definition of functions or predicates,
* to state mathematical theorems and software specifications,
* to develop interactively formal proofs of these theorems,
* to check these proofs by a small certification "kernel".
Coq is based on a logical framework called "Calculus of Inductive
Constructions" extended by a modular development system for
theories.
Homepage:https://rocq-prover.org
https://github.com/rocq-prover/rocq/
coq-serapi
- Ebuilds: 1, Testing: 0.20.0 Description:
SerAPI is a library for machine-to-machine interaction with the Coq proof
assistant, with particular emphasis on applications in IDEs, code analysis
tools, and machine learning. SerAPI provides automatic serialization of
Coq's internal OCaml datatypes from/to JSON or S-expressions (sexps).
SerAPI is a proof-of-concept and should be considered alpha-quality.
Homepage:https://github.com/ejgallego/coq-serapi/
coq-stdlib
- Ebuilds: 2, Stable: 9.0.0-r1, Testing: 9.1.0 Description: Stdlib for the Coq/Rocq Prover, used to be part of Coq
Homepage:https://github.com/coq/stdlib
cryptominisat
- Ebuilds: 1, Testing: 5.11.21-r2 Description:
This system provides CryptoMiniSat, an advanced incremental SAT solver.
The system has 3 interfaces: command-line, C++ library and python.
The command-line interface takes a cnf as an input in the DIMACS format
with the extension of XOR clauses. The C++ and python interface mimics this
and also allows for incremental use: assumptions and multiple solve calls.
Homepage:https://github.com/msoos/cryptominisat/
cubicle
- Ebuilds: 1, Testing: 1.2.0-r2 Description:
Cubicle is an open source model checker for verifying safety properties of
array-based systems. This is a syntactically restricted class of
parametrized transition systems with states represented as arrays indexed
by an arbitrary number of processes. Cache coherence protocols and mutual
exclusion algorithms are typical examples of such systems. Cubicle
model-checks by a symbolic backward reachability analysis on infinite sets
of states represented by specific simple formulas, called cubes. Cubicle is
based on ideas introduced by MCMT from which, in addition to revealing the
implementation details, it differs in a more friendly input language and a
concurrent architecture. Cubicle is written in OCaml. Its SMT solver is a
tightly integrated, lightweight and enhanced version of Alt-Ergo; and its
parallel implementation relies on the Functory library.
Homepage:https://cubicle.lri.fr/
https://github.com/cubicle-model-checker/cubicle/ License: Apache-2.0
cudd
- Ebuilds: 1, Testing: 3.0.0 Description:
CUDD stands for Colorado University Decision Diagram. It is a package for
the manipulation of Binary Decision Diagrams (BDDs), Algebraic Decision
Diagrams (ADDs) and Zero-suppressed Binary Decision Diagrams (ZDDs).
Homepage:https://davidkebo.com/cudd/ License: BSD
cvc4
- Ebuilds: 1, Testing: 1.8-r7 Description:
CVC4 is an efficient open-source automatic theorem prover for
satisfiability modulo theories (SMT) problems. It can be used to prove
the validity (or, dually, the satisfiability) of first-order formulas
in a large number of built-in logical theories and their combination.
Homepage:https://cvc4.github.io/ License: GPL-2
dataplot
- Ebuilds: 1, Testing: 20131220 Description:
Dataplot is a software system for scientific visualization,
statistical analysis, and non-linear modeling. The target Dataplot
user is the researcher and analyst engaged in the characterization,
modeling, visualization, analysis, monitoring, and optimization of
scientific and engineering processes (original version:1978).
Gentoo version adds autotools to facilitate building and robustness.
Homepage:https://www.itl.nist.gov/div898/software/dataplot/ License: public-domain
dsfmt
- Ebuilds: 1, Testing: 2.2.4 Description:
The purpose of Double precision SIMD-oriented Fast Mersenne Twister (dSFMT)
is to speed up the generation by avoiding the expensive conversion
of integer to double (floating point). dSFMT directly generates
double precision floating point pseudorandom numbers which have the
IEEE Standard for Binary Floating-Point Arithmetic (ANSI/IEEE Std
754-1985) format. dSFMT is only available on the CPUs which use IEEE
754 format double precision floating point numbers.
Homepage:http://www.math.sci.hiroshima-u.ac.jp/~m-mat/MT/SFMT License: BSD
easycrypt
- Ebuilds: 3, Testing: 2026.03 Description:
EasyCrypt is a toolset for reasoning about relational properties of
probabilistic computations with adversarial code. Its main application is
the construction and verification of game-based cryptographic proofs.
Homepage:https://github.com/EasyCrypt/easycrypt/
eclib
- Ebuilds: 1, Stable: 20250627, Testing: 20250627 Description: Programs for elliptic curves defined over the rational numbers
Homepage:https://github.com/JohnCremona/eclib License: GPL-2+ LGPL-2.1+
eprover
- Ebuilds: 2, Testing: 3.2.5 Description:
E is a theorem prover for full first-order logic with equality. It accepts
a problem specification, typically consisting of a number of first-order
clauses or formulas, and a conjecture, again either in clausal or full
first-order form. The system will then try to find a formal proof for the
conjecture, assuming the axioms. If a proof is found, the system can
provide a detailed list of proof steps that can be individually verified.
If the conjecture is existential (i.e. it is of the form "there exists an X
with property P"), more recent versions can also provide possible answers
(values for X). Development of E started as part of the E-SETHEO project at
TUM. The first public release was in in 1998, and the system has been
continuously improved ever since. I believe that E now is one of the most
powerful and friendly reasoning systems for first-order logic. The prover
has successfully participated in many competitions.
Homepage:https://www.eprover.org/
https://github.com/eprover/eprover/
fann
- Ebuilds: 2, Testing: 2.2.0-r2 Description:
Fast Artificial Neural Network Library implements multilayer artificial
neural networks in C with support for both fully connected and sparsely
connected networks. Cross-platform execution in both fixed and floating
point are supported. It includes a framework for easy handling of
training data sets. It is easy to use, versatile, well documented, and
fast. Delphi, PHP, Python and other bindings are available.
Homepage:https://leenissen.dk License: LGPL-2.1
flint
- Ebuilds: 3, Stable: 3.1.3_p1-r4, Testing: 3.4.0-r1 Description: Fast Library for Number Theory
Homepage:https://www.flintlib.org/ License: LGPL-2.1+
flocq
- Ebuilds: 1, Testing: 4.2.1 Description:
Flocq (Floats for Coq) is a formalization of floating-point arithmetic for
the Coq proof assistant. It provides a comprehensive library of theorems on
a multi-radix multi-precision arithmetic. It also supports efficient
numerical computations inside Coq.
Homepage:http://flocq.gforge.inria.fr/
https://gitlab.inria.fr/flocq/flocq/ License: LGPL-3
gap
- Ebuilds: 2, Stable: 4.14.0-r1, Testing: 4.15.1 Description:
Groups, Algorithms, Programming is a system for computational
discrete algebra, with particular emphasis on Computational Group
Theory. GAP provides a programming language, a library of thousands
of functions implementing algebraic algorithms written in the GAP
language as well as large data libraries of algebraic objects. GAP
is used in research and teaching for studying groups and their
representations, rings, vector spaces, algebras, combinatorial
structures, and more.
Homepage:https://www.gap-system.org/ License: GPL-2+
gappa
- Ebuilds: 2, Testing: 1.4.2 Description:
Gappa (Génération Automatique de Preuves de Propriétés Arithmétiques --
automatic proof generation of arithmetic properties) is a tool intended to
help verifying and formally proving properties on numerical programs
dealing with floating-point or fixed-point arithmetic.
Homepage:https://gappa.gitlabpages.inria.fr/
https://gitlab.inria.fr/gappa/gappa/ License: CeCILL-2 GPL-3+
genius
- Ebuilds: 1, Stable: 1.0.27, Testing: 1.0.27 Description:
Genius is a calculator program which can work
with arbitrary precision integers, multiple precision floats,
rational numbers, complex numbers, linear algebra, number theory,
numerical calculus, statistics, numerical equation solving,
combinatorics, elementary functions, modular arithmetic.
It has a programming language with automatic typing.
It can do various 2D and 3D plots, with possibility
to export to eps or png. Genius has a GUI IDE.
It can output matrices in LaTeX, Troff (eqn) or MathML.
Homepage:https://www.jirka.org/genius.html License: GPL-3+
gfan
- Ebuilds: 2, Stable: 0.6.2-r7, Testing: 0.6.2-r8 Description:
Gfan is a software package for computing Gröbner fans and tropical
varieties. These are polyhedral fans associated to polynomial
ideals. The maximal cones of a Gröbner fan are in bijection with the
marked reduced Gröbner bases of its defining ideal. The software
computes all marked reduced Gröbner bases of an ideal. Their union
is a universal Gröbner basis. The tropical variety of a polynomial
ideal is a certain subcomplex of the Gröbner fan. Gfan contains
algorithms for computing this complex for general ideals and
specialized algorithms for tropical curves, tropical hypersurfaces
and tropical varieties of prime ideals. In addition to the above
core functions the package contains many tools which are useful in
the study of Gröbner bases, initial ideals and tropical
geometry. The full list of commands can be found in Appendix B of
the manual. For ordinary Gröbner basis computations Gfan is not
competitive in speed compared to programs such as CoCoA, Singular
and Macaulay2.
Homepage:https://users-math.au.dk/~jensen/software/gfan/gfan.html License: GPL-2+
giac
- Ebuilds: 1, Stable: 1.9.0.995-r2, Testing: 1.9.0.995-r2 Description:
Giac is a free computer algebra system that can be used to perform
computer algebra, function graphs, interactive geometry (2-d and
3-d), spreadsheet and statistics, programmation. It may be used as
a replacement for high end graphic calculators for example on
netbooks (for about the same price as a calculator but with much
more performances).
Homepage:https://www-fourier.ujf-grenoble.fr/~parisse/giac.html License: GPL-3+
gimps
- Ebuilds: 4, Stable: 30.19.20, Testing: 30.19.20, 30.19.14 Description: The Great Internet Mersenne Prime Search
Homepage:https://www.mersenne.org/ License: GIMPS
ginac
- Ebuilds: 2, Stable: 1.8.9, Testing: 1.8.10 Description:
GiNaC is an iterated and recursive acronym for GiNaC is Not a CAS,
where CAS stands for Computer Algebra System. It is designed to allow
the creation of integrated systems that embed symbolic manipulations
together with more established areas of computer science (like
computation-intense numeric applications, graphical interfaces, etc.)
under one roof.
Homepage:https://www.ginac.de/ License: GPL-2+
glpk
- Ebuilds: 2, Stable: 5.0-r3, Testing: 5.0-r4 Description:
The GNU Linear Programming Kit package is intended for solving
large-scale linear programming (LP), mixed integer programming
(MIP), and other related problems. It is a set of routines written
in ANSI C and organized in the form of a callable library.
Homepage:https://www.gnu.org/software/glpk/ License: GPL-3
gmm
- Ebuilds: 1, Stable: 5.4.2, Testing: 5.4.2 Description:
Gmm++ is a generic C++ template library for sparse, dense and
skyline matrices. It is built as a set of generic algorithms (mult,
add, copy, sub-matrices, dense and sparse solvers ...) for any
interfaced vector type or matrix type. It can be view as a glue
library allowing cooperation between several vector and matrix
types. However, basic sparse, dense and skyline matrix/vector types
are built in Gmm++, hence it can be used as a standalone linear
algebra library.
Homepage:http://getfem.org/gmm.html License: || ( LGPL-3 LGPL-3-with-linking-exception )
gp2c
- Ebuilds: 2, Stable: 0.0.12, Testing: 0.0.14 Description:
The gp2c compiler is a package for translating GP routines into the C
programming language, so that they can be compiled and used with the PARI
system or the GP calculator.
Homepage:https://pari.math.u-bordeaux.fr/ License: GPL-2+
gretl
- Ebuilds: 1, Testing: 2021d Description:
GNU Regression, Econometrics and Time-series Library provides
a library which comprises various functions relating to econometric
estimation, a command-line client program and a GUI. The library is
based on the stand-alone command-line econometrics program ESL,
originally written by Ramu Ramanathan of the Department of Economics
at UC-San Diego. The interfaces offer several least-squares based
estimators. Besides reading data files in its own format it also
reads RATS 4 databases. It has a built-in spreadsheet for editing
data, and uses gnuplot for graphing. It can output regression results
in LaTeX format.
Homepage:http://gretl.sourceforge.net/ License: GPL-3
gsl-shell
- Ebuilds: 1, Testing: 2.3.5 Description:
GSL shell offers an interactive command-line interface
that gives access to GSL collection of mathematical functions.
GSL shell is based on the powerful and elegant scripting language Lua.
GSL shell is not just a wrapper over the C API of GSL
but does offer much more simple and expressive way to use GSL.
The objective of GSL shell is to give the user the power
of easily access GSL functions without having to write a complete C application.
Homepage:https://www.nongnu.org/gsl-shell/ License: GPL-3
jags
- Ebuilds: 1, Stable: 4.3.1-r1, Testing: 4.3.1-r1 Description:
JAGS is Just Another Gibbs Sampler. It is a program for analysis of
Bayesian hierarchical models using Markov Chain Monte Carlo (MCMC)
simulation not wholly unlike BUGS.
JAGS was written with three aims in mind:
* To have an engine for the BUGS language that runs on Unix
* To be extensible, allowing users to write their own functions,
distributions and samplers.
* To be a plaftorm for experimentation with ideas in Bayesian modelling
Homepage:https://mcmc-jags.sourceforge.io/ License: GPL-2
kind2
- Ebuilds: 1, Testing: 1.9.0 Description:
Kind 2 is an open-source, multi-engine, SMT-based automatic model checker
for safety properties of finite-state or infinite-state synchronous
reactive systems expressed as in an extension of the Lustre language. In
its basic configuration it takes as input one or more Lustre files
annotated with properties to be proven invariant, and outputs for each
property either a confirmation or a counterexample, i.e., a sequence inputs
that falsifies the property. More advanced features include contract-based
compositional verification, proof generation for proven properties, and
contract-based test generation.
Homepage:https://kind2-mc.github.io/kind2/
https://github.com/kind2-mc/kind2/
kissat
- Ebuilds: 1, Testing: 3.1.1-r1 Description:
Kissat is a "keep it simple and clean bare metal SAT solver" written in C.
It is a port of CaDiCaL back to C with improved data structures, better
scheduling of inprocessing and optimized algorithms and implementation.
Coincidentally "kissat" also means "cats" in Finnish.
Homepage:http://fmv.jku.at/kissat/
https://github.com/arminbiere/kissat/ License: MIT
lcalc
- Ebuilds: 1, Stable: 2.1.1, Testing: 2.1.1 Description: Command-line utility and library for L-function computations
Homepage:https://gitlab.com/sagemath/lcalc License: GPL-2+
lean
- Ebuilds: 2, Stable: 4.14.0-r1, Testing: 4.23.0 Description:
The Lean theorem prover is a proof assistant developed principally
by Leonardo de Moura at Microsoft Research. Lean is a functional
programming language that makes it easy to write correct and
maintainable code. You can also use Lean as an interactive theorem
prover. Lean programming primarily involves defining types and
functions. This allows your focus to remain on the problem domain and
manipulating its data, rather than the details of programming.
Homepage:https://leanprover-community.github.io/
https://github.com/leanprover/lean4/
libpoly
- Ebuilds: 1, Testing: 0.1.11 Description:
LibPoly is a C library for manipulating polynomials. The target
applications are symbolic reasoning engines, such as SMT solvers, that need
to reason about polynomial constraints. It is research software under
development, so the features and the API might change rapidly.
Homepage:https://github.com/SRI-CSL/libpoly/ License: LGPL-3+
lrcalc
- Ebuilds: 2, Stable: 2.1, Testing: 2.1 Description:
The "Littlewood-Richardson Calculator" is a package of C and Maple
programs for computing Littlewood-Richardson coefficients
Homepage:https://sites.math.rutgers.edu/~asbuch/lrcalc/ License: GPL-3+
mathematica
- Ebuilds: 6, Testing: 14.3.0-r1 Description:
Wolfram Mathematica is a software system with built-in libraries for
several areas of technical computing that allow machine learning,
statistics, symbolic computation, data manipulation, network analysis,
time series analysis, plotting functions and various types of data,
implementation of algorithms, creation of user interfaces, and interfacing
with programs written in other programming languages.
Homepage:https://www.wolfram.com/mathematica/ License: all-rights-reserved
mathomatic
- Ebuilds: 1, Stable: 16.0.5-r1, Testing: 16.0.5-r1 Description:
Mathomatic is a small, portable symbolic math program that can
automatically solve, simplify, differentiate, combine, and compare
algebraic equations, perform polynomial and complex arithmetic,
etc.
Homepage:https://github.com/mfillpot/mathomatic License: LGPL-2.1
maxima
- Ebuilds: 3, Stable: 5.47.0-r2, Testing: 5.49.0 Description:
Computer Algebra system, descendent of Macsyma.
Maxima is a system for the manipulation of symbolic and
numerical expressions, including differentiation, integration,
Taylor series, Laplace transforms, ordinary differential
equations, systems of linear equations, and vectors, matrices,
and tensors. Maxima produces high precision results by using
exact fractions and arbitrarily long floating point representations,
and can plot functions and data in two and three dimensions.
Homepage:http://maxima.sourceforge.net/ License: GPL-2 GPL-2+ LLGPL-2.1
metamath
- Ebuilds: 1, Testing: 0.198 Description:
Metamath is a tiny language that can express theorems in abstract
mathematics, accompanied by proofs that can be verified by a computer
program.
Homepage:http://us.metamath.org/
minisat
- Ebuilds: 1, Testing: 2.2.1-r1 Description:
MiniSat is a minimalistic, open-source SAT solver, developed to help
researchers and developers alike to get started on SAT. It is released
under the MIT licence, and is currently used in a number of projects.
MiniSat is small and well-documented, and possibly also well-designed,
making it an ideal starting point for adapting SAT based techniques to
domain specific problems.
Winning all the industrial categories of the SAT 2005 competition, MiniSat
is a good starting point both for future research in SAT, and for
applications using SAT.
MiniSat supports incremental SAT and has mechanisms for adding non-clausal
constraints. By virtue of being easy to modify, it is a good choice for
integrating as a backend to another tool, such as a model checker or a more
generic constraint solver.
Homepage:http://minisat.se/Main.html
https://github.com/stp/minisat/ License: MIT
msieve
- Ebuilds: 2, Testing: 1.53-r3 Description: A C library implementing a suite of algorithms to factor large integers
Homepage:https://sourceforge.net/projects/msieve/ License: public-domain
nauty
- Ebuilds: 1, Stable: 2.8.8-r1, Testing: 2.8.8-r1 Description:
nauty is a program for computing automorphism groups of graphs and digraphs. It can also produce a
canonical labelling.
nauty is written in a portable subset of C, and runs on a considerable number of different systems.
Homepage:https://pallini.di.uniroma1.it/ License: Apache-2.0
octave
- Ebuilds: 2, Stable: 9.2.0-r2, Testing: 11.1.0 Description:
Octave is a high-level language, primarily intended for numerical computations. It provides a convenient command line interface for solving linear and nonlinear problems numerically, and for performing other numerical experiments. It may also be used as a batch-oriented language.
Homepage:https://www.gnu.org/software/octave/ License: GPL-3
octave-epstk
- Ebuilds: 1, Testing: 2.4 Description:
The epsTk package provides, via a set of functions for octave, a
toolkit to create powerful encapsulated postscript (.eps) graphs. Most 2D
scientific graphics functions are written. The generated .eps-files are very
small and can be imported into other documents without loss of quality.
Homepage:http://www.epstk.de/ License: GPL-2
opensmt
- Ebuilds: 2, Testing: 2.9.2 Description:
OpenSMT2 is an SMT solver written in C++. It supports reading files in
SMT-LIB2 format and the theories QF_UF, QF_RDL, QF_IDL, QF_LRA, QF_LIA,
QF_UFLRA, QF_UFLIA and QF_AX. The system also provides an API; the
distribution includes a minimal example how to use the API.
Homepage:http://verify.inf.usi.ch/opensmt/
https://github.com/usi-verification-and-security/opensmt/
pari
- Ebuilds: 3, Stable: 2.17.1, Testing: 2.17.2 Description:
PARI is a widely used computer algebra system designed for fast
computations in number theory (factorizations, algebraic number
theory, elliptic curves...), but also contains a large number of other
useful functions to compute with mathematical entities such as
matrices, polynomials, power series, algebraic numbers, etc., and a
lot of transcendental functions.
The extra data is avaialable through use flag:
* elldata is PARI/GP version of J. E. Cremona Elliptic Curve Data,
needed by ellsearch and ellidentify.
* galdata is needed by polgalois to compute Galois group in degrees
8 through 11.
* seadata is needed by ellap for large primes.
* nftables is a repackaging of the historical megrez number field
tables (errors fixed, 1/10th the size, easier to use).
Homepage:https://pari.math.u-bordeaux.fr/ License: GPL-2+
pari-data
- Ebuilds: 1, Stable: 20191216, Testing: 20191216 Description:
The extra data for PARI consists of:
* elldata is PARI/GP version of J. E. Cremona Elliptic Curve Data,
needed by ellsearch and ellidentify.
* galdata is needed by polgalois to compute Galois group in degrees
8 through 11.
* seadata is needed by ellap for large primes.
* nftables is a repackaging of the historical megrez number field
tables (errors fixed, 1/10th the size, easier to use).
Homepage:https://pari.math.u-bordeaux.fr/packages.html License: GPL-2
plfit
- Ebuilds: 1, Stable: 1.0.1, Testing: 1.0.1 Description: Fit power-law distributions to empirical data
Homepage:https://github.com/ntamas/plfit License: BSD GPL-2+ MIT
polymake
- Ebuilds: 3, Stable: 4.15, Testing: 4.15, 4.14 Description:
Polymake is open source software for research in polyhedral
geometry. It deals with polytopes, polyhedra, and fans as well as
simplicial complexes, matroids, graphs, tropical hypersurfaces, and
other objects.
Homepage:https://polymake.org/ License: BSD GPL-2 GPL-2+ MIT WTFPL-2
prng
- Ebuilds: 1, Stable: 3.0.2-r4, Testing: 3.0.2-r4 Description:
The Pseudo-Random Number Generator library is a portable,
high-performance ANSI-C implementations of pseudorandom number
generators such as linear congruential, inversive congruential, and
explicit inversive congruential random number generators (called
LCG, ICG and EICG, respectively) created by Otmar Lendl. It is part
of the pLab project.
Homepage:http://statmath.wu.ac.at/prng/ License: GPL-2
prover9
- Ebuilds: 1, Testing: 2009.11a-r2 Description:
Prover9 and Mace4 Prover9 is an automated theorem prover for
first-order and equational logic, and Mace4 searches for finite
models and counterexamples. Prover9 is the successor of the
Otter prover.
Homepage:https://www.cs.unm.edu/~mccune/mace4/ License: GPL-2
proverif
- Ebuilds: 3, Testing: 9999 Description:
ProVerif is an automatic cryptographic protocol verifier, in the formal
model (so called Dolev-Yao model). This protocol verifier is based on a
representation of the protocol by Horn clauses. Its main features are: 1)
It can handle many different cryptographic primitives, including shared-
and public-key cryptography (encryption and signatures), hash functions,
and Diffie-Hellman key agreements, specified both as rewrite rules or as
equations. 2) It can handle an unbounded number of sessions of the protocol
(even in parallel) and an unbounded message space. This result has been
obtained thanks to some well-chosen approximations. This means that the
verifier can give false attacks, but if it claims that the protocol
satisfies some property, then the property is actually satisfied. The
considered resolution algorithm terminates on a large class of protocols
(the so-called "tagged" protocols). When the tool cannot prove a property,
it tries to reconstruct an attack, that is, an execution trace of the
protocol that falsifies the desired property.
Homepage:https://bblanche.gitlabpages.inria.fr/proverif/
https://gitlab.inria.fr/bblanche/proverif/
psmt2-frontend
- Ebuilds: 1, Stable: 0.4.0, Testing: 0.4.0 Description:
psmt2-frontend is an OCaml library to parse and type-check a conservative
extension of the SMT-LIB 2 standard with prenex polymorphism.
Homepage:https://github.com/OCamlPro-Coquera/psmt2-frontend License: Apache-2.0
pspp
- Ebuilds: 2, Stable: 1.6.2-r3, Testing: 2.0.1-r1 Description:
PSPP is a program for statistical analysis of sampled data. It
interprets commands in the SPSS language and produces tabular and
graphical output in ASCII, HTML, or PostScript format.
PSPP supports a large subset of SPSS's transformation language. Its
statistical procedure support is limited but growing.
PSPP has both text-based and a GTK+ based graphical user interfaces.
Homepage:https://www.gnu.org/software/pspp/pspp.html License: GPL-3+ FDL-1.3+
rngstreams
- Ebuilds: 1, Stable: 1.0.1, Testing: 1.0.1 Description:
RngStreams is a C implementation of a high quality uniform random
number generator that supports multiple "independent" streams of
uniform random numbers. It has been written by Pierre L'Ecuyer and
Richard Simard.
This is the GNU-style package maintained by Josef Leydold.
Homepage:https://statmath.wu.ac.at/software/RngStreams/ License: GPL-3
rw
- Ebuilds: 1, Stable: 0.9, Testing: 0.9 Description:
rw is a program that calculates rank-width and rank-decompositions.
It is based on ideas from "Computing rank-width exactly" by Sang-il Oum,
"Sopra una formula numerica" by Ernesto Pascal, "Generation of a Vector
from the Lexicographical Index" by B.P. Buckles and M. Lybanon and "Fast
additions on masked integers" by Michael D. Adams and David S. Wise.
Homepage:https://sourceforge.net/projects/rankwidth/ License: GPL-2+
sha1-polyml
- Ebuilds: 1, Testing: 5.9 Description:
<pkg>sci-mathematics/sha1-polyml</pkg> is the implementation of SHA1 taken from
the GNU coreutils package as described in the <pkg>sci-mathematics/sha1-polyml</pkg>
README.
Homepage:https://isabelle.in.tum.de/ License: GPL-3
stp
- Ebuilds: 2, Testing: 2.3.4 Description:
STP is a constraint solver (or SMT solver) aimed at solving
constraints of bitvectors and arrays. These types of
constraints can be generated by program analysis tools, theorem
provers, automated bug finders, cryptographic attack tools,
intelligent fuzzers, model checkers, and by many other
applications.
Homepage:https://stp.github.io/
https://github.com/stp/stp/
twelf
- Ebuilds: 1, Testing: 1.7.1-r2 Description:
Twelf is an implementation of the logical framework LF. It is used for
logic programming and for the formalization of programming language
theory.
Homepage:https://twelf.org/ License: BSD-2
unuran
- Ebuilds: 2, Stable: 1.9.0, Testing: 1.9.0 Description:
UNU.RAN is an ANSI C library licensed under GPL.
It contains universal (also called automatic or black-box) algorithms
that can generate random numbers from large classes of continuous or
discrete distributions, and also from practically all standard
distributions.
Homepage:https://statmath.wu.ac.at/unuran/ License: GPL-2
vampire
- Ebuilds: 2, Testing: 5.0.0 Description:
Vampire is a theorem prover, that is, a system able to prove theorems —
although now it can do much more! Its main focus is in proving theorems in
first-order logic but it can also prove non-theorems and build finite
models, as well as reasoning in combinations of theories, such as
arithmetic, arrays, and datatypes, and with higher-order logic.
The development of Vampire began in 1994 and has survived a number of
rewritings.
Homepage:https://vprover.github.io/
https://github.com/vprover/vampire/
verifpal
- Ebuilds: 1, Testing: 0.27.0 Description:
Verifpal is new software for verifying the security of cryptographic
protocols. Building upon contemporary research in symbolic formal
verification, Verifpal’s main aim is to appeal more to real-world
practitioners, students and engineers without sacrificing comprehensive
formal verification features.
Homepage:https://verifpal.com/
https://source.symbolic.software/verifpal/verifpal/ License: GPL-3+
verit
- Ebuilds: 1, Testing: 2021.06.2 Description:
veriT is a SMT (Satisfiability Modulo Theories) solver. It is open-source,
proof-producing, and complete for quantifier-free formulas with
uninterpreted functions and linear arithmetic on real numbers and integers.
It also offers good support for quantifiers.
The input format is the SMT-LIB 2.0 language and DIMACS.
Homepage:https://verit.loria.fr/ License: BSD
why3
- Ebuilds: 5, Testing: 1.8.2 Description:
Why3 is a platform for deductive program verification. It provides
a rich language for specification and programming, called WhyML,
and relies on external theorem provers, both automated and interactive,
to discharge verification conditions. Why3 comes with a standard
library of logical theories (integer and real arithmetic, Boolean
operations, sets and maps, etc.) and basic programming data structures
(arrays, queues, hash tables, etc.). A user can write WhyML programs
directly and get correct-by-construction OCaml programs through an
automated extraction mechanism. WhyML is also used as an intermediate
language for the verification of C, Java, or Ada programs.
Homepage:https://www.why3.org/
https://gitlab.inria.fr/why3/why3/ License: LGPL-2
why3-for-spark
- Ebuilds: 1, Stable: 2023.12.13-r2, Testing: 2023.12.13-r2 Description:
Why3 is a platform for deductive program verification. It provides a
rich language for specification and programming, called WhyML, and
relies on external theorem provers, both automated and interactive, to
discharge verification conditions. Why3 comes with a standard library
of logical theories (integer and real arithmetic, Boolean operations,
sets and maps, etc.) and basic programming data structures (arrays,
queues, hash tables, etc.). A user can write WhyML programs directly
and get correct-by-construction OCaml programs through an automated
extraction mechanism. WhyML is also used as an intermediate language
for the verification of C, Java, or Ada programs.
Homepage:https://www.why3.org/ https://github.com/AdaCore/why3 License: GPL-3
wxmaxima
- Ebuilds: 2, Stable: 25.04.0-r2, Testing: 26.01.0 Description:
wxMaxima is a wxWidgets GUI for the computer algebra system maxima.
Most of maxima functions are accessible through menus, some have
dialogs. The input line has command history (up-key, down-key) and
completion based on previous input (tab-key).
wxMaxima provides 2d formated display of maxima output.
Homepage:https://wxmaxima-developers.github.io/wxmaxima/ License: GPL-2
yacas
- Ebuilds: 1, Testing: 1.9.1-r2 Description:
Yacas (Yet Another Computer Algebra System) is a small and highly
flexible general-purpose computer algebra language. The syntax uses a
infix-operator grammar parser. The distribution contains a small
library of mathematical functions, but its real strength is in the
language in which you can easily write your own symbolic manipulation
algorithms.
Homepage:https://www.yacas.org/ License: GPL-2
yices2
- Ebuilds: 1, Testing: 2.6.5 Description:
Yices 2 is an SMT solver that decides the satisfiability of formulas
containing uninterpreted function symbols with equality, real and integer
arithmetic, bitvectors, scalar types, and tuples. Yices 2 supports both
linear and nonlinear arithmetic. Yices 2 can process input written in the
SMT-LIB notation (both versions 2.0 and 1.2 are supported). Alternatively,
you can write specifications using Yices 2's own specification language,
which includes tuples and scalar types. You can also use Yices 2 as a
library in your software.
Homepage:https://github.com/SRI-CSL/yices2/
z3
- Ebuilds: 5, Stable: 4.15.4, Testing: 4.16.0 Description:
Z3 is an efficient Satisfiability Modulo Theories (SMT) solver from
Microsoft Research. Z3 is a solver for symbolic logic, a foundation for
many software engineering tools. SMT solvers rely on a tight integration of
specialized engines of proof. Each engine owns a piece of the global puzzle
and implements specialized algorithms. For example, Z3’s engine for
arithmetic integrates Simplex, cuts and polynomial reasoning, while an
engine for strings are regular expressions integrate methods for symbolic
derivatives of regular languages. A theme shared among many of the
algorithms is how they exploit a duality between finding satisfying
solutions and finding refutation proofs. The solver also integrates engines
for global and local inferences and global propagation. Z3 is used in a
wide range of software engineering applications, ranging from program
verification, compiler validation, testing, fuzzing using dynamic symbolic
execution, model-based software development, network verification, and
optimization.
Homepage:https://github.com/Z3Prover/z3/ License: MIT