METIS is a set of serial programs for partitioning graphs, partitioning finite element meshes, and producing fill-reducing orderings for sparse matrices. The algorithms implemented in METIS are based on the multilevel recursive-bisection, multilevel k-way, and multi-constraint partitioning schemes.

The C-library cddlib implements the Double Description Method of Motzkin et al. for generating all vertices (i.e. extreme points) and extreme rays of a general convex polyhedron given by a system of linear inequalities in arbitrary dimension. It can also be used for the converse operation of computing convex hulls.

Aris is a program for performing logical proofs. It supports propositional and predicate logic, as well as Boolean algebra and arithmetical logic. In addition to its predefined inference and equivalence rules, Aris also supports references to older proofs. Its use of standard logical symbols and its natural deduction interface make it easy to use for beginners.

This package provides a Mathics3 frontend for Jupyter Notebook and Marimo.

mCRL2 (micro Common Representation Language 2) is a formal specification language for describing concurrent discrete event systems. Its toolset supports analysis and automatic verification, linearisation, simulation, state-space exploration and generation, and tools to optimise and analyse specifications. Also, state spaces can be manipulated, visualised and analysed.

Fast Downward is a portfolio-based planning system that supports the propositional fragment of PDDL2.2.

On modern CPUs and GPUs, integer division is several times slower than multiplication. FXdiv implements an algorithm to replace an integer division with a multiplication and two shifts. This algorithm improves performance when an application performs repeated divisions by the same divisor.

SPEX is a set of routines for sparse exact linear algebra. It contains the SPEX Left LU library for computing a sparse exact left-looking LU factorization for solving unsymmetric sparse linear systems.

The C code of lrslib implements the reverse search algorithm for vertex enumeration and convex hull problems. Its input file format is compatible with cddlib. All computations are done exactly in either multiple precision or fixed integer arithmetic. Output is not stored in memory, so even problems with very large output sizes can sometimes be solved.

Blitz++ is a C++ template class library that provides high-performance multidimensional array containers for scientific computing.

SUNDIALS is a family of software packages implemented with the goal of providing robust time integrators and nonlinear solvers that can easily be incorporated into existing simulation codes.

Armadillo is a C++ linear algebra library, aiming towards a good balance between speed and ease of use. It is useful for algorithm development directly in C++, or quick conversion of research code into production environments. It can be used for machine learning, pattern recognition, signal processing, bioinformatics, statistics, econometrics, etc. The library provides efficient classes for vectors, matrices and cubes, as well as 150+ associated functions (e.g., contiguous and non-contiguous submatrix views).

AIGER is a format, library and set of utilities for AIGs. The focus is on conversion utilities and a generic reader and writer API.

This is a header-only C++ library for calculating analytical derivatives and taylor expansions of composite functions.

HDF4 is a library and multi-object file format for storing and managing data between machines. HDF4 is an older hierarchical data format, incompatible with HDF5.

A pure Ruby AsciiMath parsing and conversion library. AsciiMath is an easy-to-write markup language for mathematics.

MUMPS (MUltifrontal Massively Parallel sparse direct Solver) solves a sparse system of linear equations A x = b using Gaussian elimination.

libflame is a portable library for dense matrix computations, providing much of the functionality present in LAPACK, developed by current and former members of the SHPC group in the Institute for Computational Engineering and Sciences at The University of Texas at Austin. libflame includes a compatibility layer, lapack2flame, which includes a complete LAPACK implementation.

The Combinatorial BLAS (CombBLAS) is an extensible distributed-memory parallel graph library offering a small but powerful set of linear algebra primitives specifically targeting graph analytics.

SCOTCH is a set of programs and libraries which implement the static mapping and sparse matrix reordering algorithms developed within the SCOTCH project. Its purpose is to apply graph theory, with a divide and conquer approach, to scientific computing problems such as graph and mesh partitioning, static mapping, and sparse matrix ordering, in application domains ranging from structural mechanics to operating systems or bio-chemistry.

OpenBLAS is a Basic Linear Algebra Subprograms (BLAS) library forked from the GotoBLAS2-1.13 BSD version.

Kiwi is an efficient C++ implementation of the Cassowary constraint solving algorithm. Kiwi has been designed from the ground up to be lightweight and fast. Kiwi ranges from 10x to 500x faster than the original Cassowary solver with typical use cases gaining a 40x improvement. Memory savings are consistently > 5x.

Why3 provides a 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.

This DUNE module provides interface and implementation for shape functions defined on the DUNE reference elements. In addition to the shape function, interpolation operators and special keys are provided which can be used to assemble global function spaces on finite-element grids.

This package provides an interface and implementation for shape functions defined on the DUNE reference elements. In addition to the shape function, interpolation operators and special keys are provided which can be used to assemble global function spaces on finite-element grids.