{"category":{"categoryid":317,"name":"sci-mathematics","summary":"The sci-mathematics category contains mathematical software."},"packages":[{"categoryid":317,"description":"Software package for algebraic, geometric and combinatorial problems","firstseen":"2010-10-20T14:34:09.960833","maintainer":"tomka@gentoo.org","maintainername":"Thomas Kahle","name":"4ti2","packageid":56409,"summary":"4ti2 is a software package for algebraic, geometric and combinatorial problems on linear spaces and for toric ideals too."},{"categoryid":317,"description":"System for sequential logic synthesis and formal verification","firstseen":"2023-03-13T22:02:03.272341","name":"abc","packageid":75902,"summary":"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."},{"categoryid":317,"description":"Industrial strength theorem prover, logic and programming language","firstseen":"2023-01-08T00:45:43.083723","name":"acl2","packageid":75742,"summary":"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."},{"categoryid":317,"description":"Toolkit for literate programming in Coq","firstseen":"2022-03-05T04:57:32.030109","name":"alectryon","packageid":74527,"summary":"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."},{"categoryid":317,"description":"Automatic theorem prover","firstseen":"2017-10-14T07:25:18.254331","name":"alt-ergo","packageid":68081,"summary":"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."},{"categoryid":317,"description":"C library for arbitrary-precision interval arithmetic","firstseen":"2017-07-25T20:08:34.814720","name":"arb","packageid":67908,"summary":"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."},{"categoryid":317,"description":"Software for Numerical Algebraic Geometry","firstseen":"2013-08-05T13:36:38.436767","maintainer":"tomka@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"bertini","packageid":61079,"summary":"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."},{"categoryid":317,"description":"Fast SMT solver for bit-vectors, arrays and uninterpreted functions","firstseen":"2023-01-11T04:08:58.040421","name":"boolector","packageid":75749,"summary":"Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions. It supports the SMT-LIB logics BV, QF_ABV, QF_AUFBV, QF_BV and QF_UFBV. Boolector provides a rich C and Python API and supports incremental solving, both with the SMT-LIB commands push and pop, and as solving under assumptions."},{"categoryid":317,"description":"Generic parser and tools for the BTOR2 format","firstseen":"2023-01-11T04:08:58.040421","name":"btor2tools","packageid":75750},{"categoryid":317,"description":"Field-theory motivated approach to computer algebra","firstseen":"2022-03-01T21:39:51.259609","name":"cadabra","packageid":74518,"summary":"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."},{"categoryid":317,"description":"Simplified Satisfiability Solver","firstseen":"2021-12-28T15:08:33.247115","name":"cadical","packageid":73921,"summary":"The goal of CaDiCaL is to provide a clean and efficient state-of-the-art CDCL solver, which is also easy to understand and change."},{"categoryid":317,"description":"Arbitrary precision C-like arithmetic system","firstseen":"2010-05-04T00:54:45.661860","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"calc","packageid":41977,"summary":"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."},{"categoryid":317,"description":"C++ library for geometric algorithms and data structures","firstseen":"2010-05-04T00:54:45.661860","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"cgal","packageid":48858,"summary":"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."},{"categoryid":317,"description":"Polygon Clipping and Offsetting","firstseen":"2024-11-16T22:07:48.489867","name":"clipper2","packageid":77861},{"categoryid":317,"description":"C routines for finding cliques in an arbitrary weighted graph","firstseen":"2020-01-31T16:15:36.110058","name":"cliquer","packageid":70767},{"categoryid":317,"description":"Coq\/Rocq is a proof assistant written in O'Caml","firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"coq","packageid":42174,"summary":"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."},{"categoryid":317,"description":"Mathematical Components for the Coq proof assistant","firstseen":"2022-03-05T04:57:32.030109","name":"coq-mathcomp","packageid":74528},{"categoryid":317,"description":"Serialization library and protocol for interaction with the Coq proof assistant","firstseen":"2022-03-05T04:57:32.030109","name":"coq-serapi","packageid":74529,"summary":"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."},{"categoryid":317,"description":"Stdlib for the Coq\/Rocq Prover, used to be part of Coq","firstseen":"2025-03-16T21:36:59.045185","name":"coq-stdlib","packageid":78227},{"categoryid":317,"description":"Advanced SAT solver with C++ and command-line interfaces","firstseen":"2021-12-26T20:23:15.104272","name":"cryptominisat","packageid":73913,"summary":"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."},{"categoryid":317,"description":"Model checker for verifying properties of array-based systems","firstseen":"2023-01-10T23:47:47.966911","name":"cubicle","packageid":75748,"summary":"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."},{"categoryid":317,"description":"Colorado University binary Decision Diagram library","firstseen":"2022-12-18T22:22:04.912741","name":"cudd","packageid":75682,"summary":"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)."},{"categoryid":317,"description":"Automatic theorem prover for satisfiability modulo theories (SMT) problems","firstseen":"2018-07-18T22:57:31.709458","name":"cvc4","packageid":69283,"summary":"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."},{"categoryid":317,"description":"Program for scientific visualization and statistical analyis","firstseen":"2010-05-04T00:54:45.661860","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"dataplot","packageid":44663,"summary":"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."},{"categoryid":317,"description":"Calculation of some eigenvectors of a large real, symmetrical, matrix","firstseen":"2012-03-22T15:06:18.781906","maintainer":"sci-chemistry@gentoo.org","maintainername":"Gentoo Chemistry Project","name":"diagrtb","packageid":59043,"summary":"A fortran program for the calculation of some eigenvectors of a large real, symmetrical, matrix. If the matrix was obtained, for instance, with the PDBMAT program, these eigenvectors correspond to the low-frequency normal modes (i.e., mostly those with a collective character) of the system. Note that in the case of proteins, low-frequency normal modes thus obtained are found to be very close to those obtained with standard, much more realistic (e.g., all atoms with empirical force fields), models. The method used rests upon the RTB approximation (standing for Rotations-Translations-of-Blocks). Within the frame of this approximation, blocks of n (n=1,2,...) consecutive monomers (amino-acid residues) are assumed to behave like rigid bodies. Requirements: a matrix in the \"i j non-zero-ij-matrix-element\" format. A file with the coordinates of the system, in the PDB or \"x y z mass block-number\" format."},{"categoryid":317,"description":"Double precision SIMD-oriented Fast Mersenne Twister library","firstseen":"2021-04-08T04:09:24.581438","name":"dsfmt","packageid":72662,"summary":"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."},{"categoryid":317,"description":"Python library to solve linear games over symmetric cones","firstseen":"2016-11-16T14:35:56.785762","name":"dunshire","packageid":66107},{"categoryid":317,"description":"Computer-Aided Cryptographic Proofs","firstseen":"2021-12-12T02:08:52.137547","name":"easycrypt","packageid":73746,"summary":"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."},{"categoryid":317,"description":"Programs for elliptic curves defined over the rational numbers","firstseen":"2019-12-30T15:16:14.207852","name":"eclib","packageid":70548},{"categoryid":317,"description":"Random number sequence test and entropy calculation","firstseen":"2010-12-03T14:48:10.692416","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"ent","packageid":56590},{"categoryid":317,"description":"Automated theorem prover for full first-order logic with equality","firstseen":"2023-01-04T04:03:07.398053","name":"eprover","packageid":75732,"summary":"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."},{"categoryid":317,"description":"Mathematical programming environment","firstseen":"2010-05-04T00:54:45.661860","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"euler","packageid":53619},{"categoryid":317,"description":"Fast Artificial Neural Network Library","firstseen":"2010-05-04T00:54:45.661860","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"fann","packageid":51043,"summary":"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."},{"categoryid":317,"description":"Fast Library for Number Theory","firstseen":"2012-11-26T14:36:35.780422","maintainer":"patrick@gentoo.org","maintainername":"Patrick Lauer","name":"flint","packageid":60059},{"categoryid":317,"description":"Formalization of floating-point arithmetic for the Coq proof assistant","firstseen":"2022-12-24T22:51:22.910451","name":"flocq","packageid":75711,"summary":"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."},{"categoryid":317,"description":"Symbolic Manipulation System","firstseen":"2012-05-31T14:37:38.495311","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"form","packageid":59408},{"categoryid":317,"description":"FriCAS is a fork of Axiom computer algebra system","firstseen":"2010-05-04T00:54:45.661860","maintainer":"grozin@gentoo.org","maintainername":"Andrey Grozin","name":"fricas","packageid":42643},{"categoryid":317,"description":"Software system and project for computations with monomial ideals","firstseen":"2010-11-07T14:34:04.346709","maintainer":"tomka@gentoo.org","maintainername":"Thomas Kahle","name":"frobby","packageid":56491},{"categoryid":317,"description":"System for computational discrete algebra. Core functionality.","firstseen":"2024-01-22T11:43:13.819329","name":"gap","packageid":77034,"summary":"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."},{"categoryid":317,"description":"Tool for verifying floating-point or fixed-point arithmetic","firstseen":"2022-12-24T22:51:22.910451","name":"gappa","packageid":75712,"summary":"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."},{"categoryid":317,"description":"Allows the certificates Gappa generates to be imported by the Coq","firstseen":"2022-12-24T22:51:22.910451","name":"gappalib-coq","packageid":75713},{"categoryid":317,"description":"Genius Mathematics Tool and the GEL Language","firstseen":"2010-05-04T00:54:45.661860","maintainer":"grozin@gentoo.org","maintainername":"Andrey Grozin","name":"genius","packageid":48092,"summary":"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."},{"categoryid":317,"description":"Mathematics software for geometry","firstseen":"2020-09-19T05:51:34.761845","name":"geogebra-bin","packageid":72021},{"categoryid":317,"description":"Interactive Geometry Viewer","firstseen":"2010-05-04T00:54:45.661860","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"geomview","packageid":50417},{"categoryid":317,"description":"Compute Groebner fans and tropical varieties","firstseen":"2010-11-13T14:34:00.987409","maintainer":"tomka@gentoo.org","maintainername":"Thomas Kahle","name":"gfan","packageid":56539,"summary":"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."},{"categoryid":317,"description":"A free C++ Computer Algebra System library and its interfaces","firstseen":"2021-04-01T23:15:11.779465","name":"giac","packageid":72650,"summary":"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)."},{"categoryid":317,"description":"The Great Internet Mersenne Prime Search","firstseen":"2010-05-04T00:54:45.661860","maintainer":"tomka@gentoo.org","maintainername":"Thomas Kahle","name":"gimps","packageid":45689},{"categoryid":317,"description":"C++ library and tools for symbolic calculations","firstseen":"2010-05-04T00:54:45.661860","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"ginac","packageid":45118,"summary":"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."},{"categoryid":317,"description":"GNU Linear Programming Kit","firstseen":"2010-05-04T00:54:45.661860","maintainer":"robbat2@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"glpk","packageid":44310,"summary":"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."},{"categoryid":317,"description":"Generic C++ template library for sparse, dense and skyline matrices","firstseen":"2010-05-04T00:54:45.661860","maintainer":"amynka@gentoo.org","name":"gmm","packageid":43779,"summary":"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."},{"categoryid":317,"description":"Elliptic Curve Method for Integer Factorization","firstseen":"2012-11-16T15:31:04.085928","maintainer":"patrick@gentoo.org","maintainername":"Patrick Lauer","name":"gmp-ecm","packageid":60000},{"categoryid":317,"description":"A GP to C translator","firstseen":"2019-12-28T14:16:43.588328","name":"gp2c","packageid":70541,"summary":"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."},{"categoryid":317,"description":"Regression, econometrics and time-series library","firstseen":"2010-05-04T00:54:45.661860","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"gretl","packageid":48475,"summary":"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."},{"categoryid":317,"description":"Lua interactive shell for sci-libs\/gsl","firstseen":"2012-09-21T13:40:25.039387","maintainer":"grozin@gentoo.org","maintainername":"Andrey Grozin","name":"gsl-shell","packageid":59829,"summary":"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."},{"categoryid":317,"description":"Just Another Gibbs Sampler for Bayesian MCMC simulation","firstseen":"2011-02-13T01:36:35.438374","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"jags","packageid":56962,"summary":"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"},{"categoryid":317,"description":"Multi-engine SMT-based automatic model checker","firstseen":"2023-06-03T18:09:22.830387","name":"kind2","packageid":76227,"summary":"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."},{"categoryid":317,"description":"Keep-it-simple and clean bare metal SAT solver written in C","firstseen":"2023-01-10T04:41:14.221763","name":"kissat","packageid":75747,"summary":"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."},{"categoryid":317,"description":"Command-line utility and library for L-function computations","firstseen":"2021-07-01T20:24:35.558593","name":"lcalc","packageid":73058},{"categoryid":317,"description":"The Lean Theorem Prover","firstseen":"2021-11-26T13:37:00.805088","name":"lean","packageid":73639,"summary":"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."},{"categoryid":317,"description":"C library for manipulating polynomials","firstseen":"2022-12-18T22:22:04.912741","name":"libpoly","packageid":75683,"summary":"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."},{"categoryid":317,"description":"Mixed Integer Linear Programming (MILP) solver","firstseen":"2011-07-24T14:38:52.845929","maintainer":"office@gentoo.org","maintainername":"Gentoo Office project","name":"lpsolve","packageid":57658},{"categoryid":317,"description":"Littlewood-Richardson Calculator","firstseen":"2020-01-02T15:39:17.494661","name":"lrcalc","packageid":70559,"summary":"The \"Littlewood-Richardson Calculator\" is a package of C and Maple programs for computing Littlewood-Richardson coefficients"},{"categoryid":317,"description":"Geometry library for topological robustness","firstseen":"2024-11-16T22:07:48.489867","name":"manifold","packageid":77862},{"categoryid":317,"description":"Wolfram Mathematica","firstseen":"2020-06-24T15:45:06.496813","name":"mathematica","packageid":71242,"summary":"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."},{"categoryid":317,"description":"Plot parametric and implicit surfaces","firstseen":"2016-03-16T14:41:27.999617","maintainer":"grozin@gentoo.org","maintainername":"Andrey Grozin","name":"mathmod","packageid":65152,"summary":"MathMod is a mathematical modeling software that visualize and animate implicit and parametric surfaces. MathMod supports: 3D and 4D plotting and animation, OBJ output file format, Textue and pigmentation support, Noise and Turbulence effects support, Large set of scripted examples."},{"categoryid":317,"description":"Automatic algebraic manipulator","firstseen":"2010-05-04T00:54:45.661860","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"mathomatic","packageid":53558,"summary":"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."},{"categoryid":317,"description":"Free computer algebra environment based on Macsyma","firstseen":"2010-05-04T00:54:45.661860","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"maxima","packageid":51555,"summary":"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."},{"categoryid":317,"description":"Proof verifier based on a minimalistic formalism","firstseen":"2021-11-26T10:11:25.030426","name":"metamath","packageid":73601,"summary":"Metamath is a tiny language that can express theorems in abstract mathematics, accompanied by proofs that can be verified by a computer program."},{"categoryid":317,"description":"Sample databases for Metamath","firstseen":"2022-03-03T05:27:02.264092","name":"metamath-databases","packageid":74524,"summary":"This is a collection of rigorously verified Metamath databases that specify mathematical axioms and formal proofs of theorems derived from those axioms."},{"categoryid":317,"description":"Small yet efficient SAT solver with reference paper","firstseen":"2011-04-10T14:39:35.202649","maintainer":"sci@gentoo.org","maintainername":"Gentoo Science Project","name":"minisat","packageid":57212,"summary":"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."},{"categoryid":317,"description":"A C library implementing a suite of algorithms to factor large integers","firstseen":"2012-11-16T15:31:04.085928","maintainer":"patrick@gentoo.org","maintainername":"Patrick Lauer","name":"msieve","packageid":60001},{"categoryid":317,"description":"Computing automorphism groups of graphs and digraphs","firstseen":"2010-10-25T14:34:29.283798","maintainer":"tomka@gentoo.org","maintainername":"Thomas Kahle","name":"nauty","packageid":56430,"summary":"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."},{"categoryid":317,"description":"A GiNaC-based library for symbolic expansion of certain transcendental functions","firstseen":"2011-01-16T14:42:12.446532","maintainer":"grozin@gentoo.org","maintainername":"Andrey Grozin","name":"nestedsums","packageid":56712},{"categoryid":317,"description":"Tool for computations in affine monoids and more","firstseen":"2010-11-03T14:34:37.319663","maintainer":"tomka@gentoo.org","maintainername":"Thomas Kahle","name":"normaliz","packageid":56474,"summary":"Normaliz is a (command line) tool for computations in affine monoids, vector configurations, lattice polytopes, and rational cones."},{"categoryid":317,"description":"A set of programs for dealing with numbers from the command line","firstseen":"2010-05-04T00:54:45.661860","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"num-utils","packageid":45329},{"categoryid":317,"description":"High-level interactive language for numerical computations","firstseen":"2010-05-04T00:54:45.661860","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"octave","packageid":45190,"summary":"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."},{"categoryid":317,"description":"Graphical output functions for Matlab and Octave","firstseen":"2011-03-10T14:37:16.203057","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"octave-epstk","packageid":57066,"summary":"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."},{"categoryid":317,"description":"Compact and open-source SMT-solver written in C++","firstseen":"2023-01-09T02:11:15.558491","name":"opensmt","packageid":75745,"summary":"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."},{"categoryid":317,"description":"An Automated Deduction System","firstseen":"2010-05-04T00:54:45.661860","maintainer":"sci@gentoo.org","maintainername":"Gentoo Science Project","name":"otter","packageid":55653},{"categoryid":317,"description":"A Package for Analyzing Lattice Polytopes (PALP)","firstseen":"2024-03-06T14:07:41.857494","name":"palp","packageid":77149},{"categoryid":317,"description":"Computer-aided number theory C library and tools","firstseen":"2010-05-04T00:54:45.661860","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"pari","packageid":45029,"summary":"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)."},{"categoryid":317,"description":"Additional dataset packages for PARI","firstseen":"2011-07-28T14:40:41.565127","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"pari-data","packageid":57675,"summary":"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)."},{"categoryid":317,"description":"Portable, Extensible Toolkit for Scientific Computation","firstseen":"2019-08-05T07:39:31.134254","name":"petsc","packageid":70044},{"categoryid":317,"description":"SAT solver with proof and core support","firstseen":"2022-12-06T02:51:40.114587","name":"picosat","packageid":75647},{"categoryid":317,"description":"The edge addition planarity suite of graph algorithms","firstseen":"2020-01-30T01:41:00.101652","name":"planarity","packageid":70766},{"categoryid":317,"description":"Fit power-law distributions to empirical data","firstseen":"2023-05-22T21:27:29.733875","name":"plfit","packageid":76181},{"categoryid":317,"description":"Tool for polyhedral geometry and combinatorics","firstseen":"2023-11-13T22:58:41.485768","name":"polymake","packageid":76731,"summary":"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."},{"categoryid":317,"description":"Highly optimized CLI and library to count primes","firstseen":"2021-12-24T13:50:00.807505","name":"primecount","packageid":73908},{"categoryid":317,"description":"CLI and library for quickly generating prime numbers","firstseen":"2021-12-24T13:50:00.807505","name":"primesieve","packageid":73909},{"categoryid":317,"description":"Pseudo-Random Number Generator library","firstseen":"2010-12-18T14:40:44.842011","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"prng","packageid":56624,"summary":"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."},{"categoryid":317,"description":"Automated theorem prover for first-order and equational logic","firstseen":"2012-01-08T16:20:08.260092","maintainer":"gienah@gentoo.org","maintainername":"Mark Wright","name":"prover9","packageid":58656,"summary":"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."},{"categoryid":317,"description":"Cryptographic protocol verifier in the formal model","firstseen":"2023-08-13T20:46:13.170863","name":"proverif","packageid":76384,"summary":"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."},{"categoryid":317,"description":"Library to parse and type-check an extension of the SMT-LIB 2 standard","firstseen":"2019-07-26T07:18:04.713000","name":"psmt2-frontend","packageid":69972,"summary":"psmt2-frontend is an OCaml library to parse and type-check a conservative extension of the SMT-LIB 2 standard with prenex polymorphism."},{"categoryid":317,"description":"Program for statistical analysis of sampled data","firstseen":"2010-05-04T00:54:45.661860","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"pspp","packageid":50818,"summary":"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."},{"categoryid":317,"description":"IDE for the R-project","firstseen":"2010-05-04T00:54:45.661860","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"rkward","packageid":54498},{"categoryid":317,"description":"Multiple independent streams of pseudo-random numbers","firstseen":"2010-12-18T14:40:44.842011","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"rngstreams","packageid":56625,"summary":"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."},{"categoryid":317,"description":"Compute rank-width decompositions of graphs","firstseen":"2015-06-23T13:38:03.727432","maintainer":"mjo@gentoo.org","maintainername":"Michael Orlitzky","name":"rw","packageid":63818,"summary":"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."},{"categoryid":317,"description":"implementation of SHA1 is taken from the GNU coreutils package","firstseen":"2012-12-08T14:37:48.924112","maintainer":"gienah@gentoo.org","maintainername":"Mark Wright","name":"sha1-polyml","packageid":60104,"summary":""},{"categoryid":317,"description":"Computer algebra system for polynomial computations","firstseen":"2010-05-04T00:54:45.661860","maintainer":"tomka@gentoo.org","maintainername":"Thomas Kahle","name":"singular","packageid":55483},{"categoryid":317,"description":"Scalable Library for Eigenvalue Problem Computations","firstseen":"2019-08-05T07:39:31.134254","name":"slepc","packageid":70045},{"categoryid":317,"description":"Interpolating SMT-solver computing Craig interpolants for various theories","firstseen":"2021-12-28T18:09:09.523053","name":"smtinterpol","packageid":73922},{"categoryid":317,"description":"An efficient logic-model checker for the verification of multi-threaded code","firstseen":"2010-05-04T00:54:45.661860","maintainer":"phajdan.jr@gentoo.org","maintainername":"Pawel Hajdan jr","name":"spin","packageid":48982},{"categoryid":317,"description":"Simple Theorem Prover, an efficient SMT solver for bitvectors","firstseen":"2021-12-27T13:30:54.463898","name":"stp","packageid":73915,"summary":"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."},{"categoryid":317,"description":"Symmetric power elliptic curve L-functions","firstseen":"2020-05-18T02:44:26.404076","name":"sympow","packageid":71151},{"categoryid":317,"description":"Computing Triangulations Of Point Configurations and Oriented Matroids","firstseen":"2010-11-10T14:55:55.581632","maintainer":"tomka@gentoo.org","maintainername":"Thomas Kahle","name":"topcom","packageid":56528},{"categoryid":317,"description":"Implementation of the logical framework LF","firstseen":"2012-12-10T14:36:29.392811","maintainer":"gienah@gentoo.org","maintainername":"Mark Wright","name":"twelf","packageid":60110,"summary":"Twelf is an implementation of the logical framework LF. It is used for logic programming and for the formalization of programming language theory."},{"categoryid":317,"description":"Universal Non-Uniform Random number generator","firstseen":"2010-12-18T14:40:44.842011","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"unuran","packageid":56626,"summary":"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."},{"categoryid":317,"description":"The Vampire Prover, theorem prover for first-order logic","firstseen":"2021-12-11T15:06:40.720898","name":"vampire","packageid":73738,"summary":"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."},{"categoryid":317,"description":"Cryptographic protocol analysis for real-world protocols","firstseen":"2023-08-13T20:46:13.170863","name":"verifpal","packageid":76385,"summary":"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."},{"categoryid":317,"description":"An open, trustable and efficient SMT-prover","firstseen":"2021-12-24T14:10:06.082751","name":"verit","packageid":73910,"summary":"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."},{"categoryid":317,"description":"Platform for deductive program verification","firstseen":"2021-12-12T02:08:52.137547","name":"why3","packageid":73747,"summary":"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."},{"categoryid":317,"description":"SPARK 2014 repository for the Why3 verification platform","firstseen":"2017-10-19T20:17:41.724443","name":"why3-for-spark","packageid":68094,"summary":"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."},{"categoryid":317,"description":"Graphical frontend to Maxima, using the wxWidgets toolkit","firstseen":"2010-05-04T00:54:45.661860","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"wxmaxima","packageid":49582,"summary":"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."},{"categoryid":317,"description":"General purpose computer algebra system","firstseen":"2010-05-04T00:54:45.661860","maintainer":"sci-mathematics@gentoo.org","maintainername":"Gentoo Mathematics Project","name":"yacas","packageid":41973,"summary":"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."},{"categoryid":317,"description":"Yet another factoring utility","firstseen":"2012-11-19T14:39:00.891770","maintainer":"patrick@gentoo.org","maintainername":"Patrick Lauer","name":"yafu","packageid":60031},{"categoryid":317,"description":"SMT Solver supporting SMT-LIB and Yices specification language","firstseen":"2022-12-18T22:22:04.912741","name":"yices2","packageid":75684,"summary":"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."},{"categoryid":317,"description":"An efficient theorem prover","firstseen":"2017-01-02T14:37:11.628924","name":"z3","packageid":66323,"summary":"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."}]}