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.

Glucose is a SAT solver based on a scoring scheme introduced in 2009 for the clause learning mechanism of so called “Modern” SAT solvers. It is designed to be parallel.

ScaLAPACK is a Fortran 90 library of high-performance linear algebra routines on parallel distributed memory machines. ScaLAPACK solves dense and banded linear systems, least squares problems, eigenvalue problems, and singular value problems.

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.

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.

Arcane is a development environment for parallel numerical calculation code. It supports the architectural aspects of a calculation code, such as data structures for meshing and parallelism, as well as more environment-related aspects such as dataset configuration.

Vc provides portable, zero-overhead C++ types for explicitly data-parallel programming. It is a library designed to ease explicit vectorization of C++ code. Its types enable explicitly stating data-parallel operations on multiple values. The parallelism is therefore added via the type system. Vc has an intuitive API and provides portability between different compilers and compiler versions as well as portability between different vector instruction sets. Thus, an application written with Vc can be compiled for:

1. AVX and AVX2

2. SSE2 up to SSE4.2 or SSE4a

3. Scalar

4. MIC

5. NEON (in development)

6. NVIDIA GPUs / CUDA (in development)

pagmo is a C++ scientific library for massively parallel optimization. It is built around the idea of providing a unified interface to optimization algorithms and to optimization problems and to make their deployment in massively parallel environments easy.

The dune-functions module provides an abstraction layer for global finite element functions. Its two main concepts are functions implemented as callable objects, and bases of finite element spaces.

GKlib is a library of various helper routines and frameworks used by software from KarypisLab, such as METIS.

CHOLMOD is a set of routines for factorizing sparse symmetrix positive definite matrices, updating/downdating sparse Cholesky factorizations and other related operations.

PETSc, pronounced PET-see (the S is silent), is a suite of data structures and routines for the scalable (parallel) solution of scientific applications modeled by partial differential equations.

This package provides the Blis BLAS-like linear algebra library, as a self-contained C-extension for Python.

PALP is a set of programs for calculations with lattice polytopes and applications to toric geometry.

Deal.II is a C++ program library targeted at the computational solution of partial differential equations using adaptive finite elements. The main aim of deal.II is to enable rapid development of modern finite element codes, using among other aspects adaptive meshes and a wide array of tools often used in finite element programs.

SuperLU is a general purpose library for the direct solution of large, sparse, nonsymmetric systems of linear equations on high performance machines. The library is written in C and is callable from either C or Fortran. The library routines perform an LU decomposition with partial pivoting and triangular system solves through forward and back substitution. The library also provides threshold-based ILU factorization preconditioners.

DUNE, the Distributed and Unified Numerics Environment is a modular toolbox for solving partial differential equations (PDEs) with grid-based methods. It supports the easy implementation of methods like Finite Elements (FE), Finite Volumes (FV), and also Finite Differences (FD).

This package contains the DUNE UG grid classes.

reduceLCS is an implementation of the Reduce-Expand algorithm for LCS. It is a fast program to compute the approximate Longest Commons Subsequence of a set of strings.

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

This header-only C++ library implements conversion to and from half-precision floating point formats.

HPCombi is a C++17 header-only library using the SSE and AVX instruction sets, and some equivalents, for very fast manipulation of combinatorial objects such as transformations, permutations, and boolean matrices of small size.

GNU Octave is a high-level interpreted language that is specialized for numerical computations. It can be used for both linear and non-linear applications and it provides great support for visualizing results. Work may be performed both at the interactive command-line as well as via script files.

bliss is a library for computing automorphism groups +and canonical forms of graphs. It has both a command line user interface as +well as C++ and C programming language APIs.

The SPQR (SuiteSparseQR) package provides sparse QR factorization based on the multifrontal method, using BLAS for the frontal matrices.