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.

Bitwuzla is a SMT solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays, uninterpreted functions and their combinations.

Z3 is a theorem prover and satisfiability modulo theories (SMT) solver. It provides a C/C++ API, as well as Python bindings.

Maxima is a system for the manipulation of symbolic and numerical expressions. It yields high precision numeric results by using exact fractions, arbitrary precision integers, and variable precision floating point numbers.

feedgnuplot is a tool to plot realtime and stored data from the command line, using gnuplot. It can read data from a pipe or file, make a variety of transformations, and render the result in the terminal or with an external viewer.

orthopy provides various orthogonal polynomial classes for lines, triangles, quadrilaterals, disks, spheres, hexahedra, and n-cubes. All computations are done using numerically stable recurrence schemes. Furthermore, all functions are fully vectorized and can return results in exact arithmetic.

This library implements the math.h functions in fixed point (16.16) format.

The terminal calculator is a small program to help users of the GNU/Linux terminal do calculations simply and quickly. The formula to be calculated can be fed to tcalc through the command line.

The dune-subgrid module marks elements of another hierarchical dune grid. The set of marked elements can then be accessed as a hierarchical dune grid in its own right. Dune-Subgrid provides the full grid interface including adaptive mesh refinement.

Ceres Solver is a C++ library for modeling and solving large, complicated optimization problems. It is a feature rich, mature and performant library which has been used in production since 2010. Ceres Solver can solve two kinds of problems:

1. non-linear least squares problems with bounds constraints;

2. general unconstrained optimization problems.

The Java HDF5 Interface (JHI5) uses the Java Native Interface to wrap the HDF5 library, which is implemented in C.

Bonmin is a code for solving general MINLP (Mixed Integer NonLinear Programming) problems. It builds on top of Cbc and Ipopt.

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

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.

SMTInterpol is an SMT solver, that can compute Craig interpolants for various theories.

This package provides a computer algebra system--an alternative to Wolfram.

LAPACK is a Fortran 90 library for solving the most commonly occurring problems in numerical linear algebra.

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.

The p4est software library enables the dynamic management of a collection of adaptive octrees, conveniently called a forest of octrees. p4est is designed to work in parallel and scales to hundreds of thousands of processor cores.

SuiteSparse is a suite of sparse matrix algorithms. This package contains a library with common configuration options.

CUDD is a library for manipulating decision diagrams. It supports binary decision diagrams, algebraic decision diagrams, and zero-suppressed binary decision diagrams.

OpenLibm is an effort to have a high quality, portable, standalone C mathematical library (libm). It can be used standalone in applications and programming language implementations. The project was born out of a need to have a good libm for the Julia programming language that worked consistently across compilers and operating systems, and in 32-bit and 64-bit environments.

The itex2MML utility is a stream filter. It takes text with embedded itex equations, converts the itex equations to MathML, and outputs the resulting text.

COLAMD is library for computing a permutation vector for a matrix with which the LU factorization becomes sparser.