NOMAD is a C++ implementation of the mesh-adaptive direct search (MADS) algorithm, designed for difficult blackbox optimization problems. These problems occur when the functions defining the objective and constraints are the result of costly computer simulations.

CGLM is an optimised 3D maths library for graphics software based on the GLSL specifications.

It's similar to the original C++ GLM library but written in C99 and compatible with C89.

DUNE, the Distributed and Unified Numerics Environment is a modular toolbox for solving partial differential equations (PDEs) with grid-based methods.

This is the iterative solver template library which provides generic sparse matrix/vector classes and a variety of solvers based on these classes. A special feature is the use of templates to exploit the recursive block structure of finite element matrices at compile time. Available solvers include Krylov methods, (block-) incomplete decompositions and aggregation-based algebraic multigrid.

HDF-EOS5 is a software library built on HDF5 to support the construction of data structures used in NASA's Earth Observing System (Grid, Point and Swath).

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.

The Interior Point Optimizer (IPOPT) is a software package for large-scale nonlinear optimization. It provides C++, C, and Fortran interfaces.

primecount is a command-line program and C/C++ library that counts the number of primes no greater than x (maximum 1031) using highly optimized implementations of the combinatorial prime counting algorithms.

This package provides a command-line interface to Mathics3.

Qhull computes the convex hull, Delaunay triangulation, Voronoi diagram, halfspace intersection about a point, furthest-site Delaunay triangulation, and furthest-site Voronoi diagram. The source code runs in 2-d, 3-d, 4-d, and higher dimensions. Qhull implements the Quickhull algorithm for computing the convex hull. It handles roundoff errors from floating point arithmetic. It computes volumes, surface areas, and approximations to the convex hull.

Qhull does not support triangulation of non-convex surfaces, mesh generation of non-convex objects, medium-sized inputs in 9-D and higher, alpha shapes, weighted Voronoi diagrams, Voronoi volumes, or constrained Delaunay triangulations.

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.

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.

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.

This package provides a Django front end for Mathics3.

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.

This package provides a Wolfram language lexer for Pygments.

HYPRE is a software library of high performance preconditioners and solvers for the solution of large, sparse linear systems of equations. It features multigrid solvers for both structured and unstructured grid problems.

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

hmat-oss is hierarchical matrix library written in C++ with a C API. It contains a LU and LLt solver, and a few other things.

SYMPOW is a mathematical program to compute special values of symmetric power elliptic curve L-functions; it can compute up to about 64 digits of precision.

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.

This package provides a range of SAT solvers, including the sequential lingeling and its parallel variants plingeling and treengeling. A bounded model checker is also included.

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.

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.

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