Release of ocplibsimplex, version 0.5
On last November, we released version 0.5 of ocplibsimplex, a generic library implementing the Simplex Algorithm in OCaml. It is a key component of the AltErgo automatic theorem prover that we keep developing at OCamlPro.
The simplex algorithm⚓
The Simplex Algorithm is well known among linear optimization enthusiasts. Let's say you own a manufacture producing two kinds of chairs: the first is cheap, you make a small profit out of them but they are quick to produce; the second one is a bit more fancy, you make a bigger profit but they need a lot of time to build. You have a limited amount of wood and time. How many cheap and fancy chairs should you produce to optimize your profits?
You can represent this problem with a set of mathematical constraints (more precisely, linear inequalities) which is precisely the scope of the simplex algorithm. Given a set of linear inequalities, it computes a solution maximizing a given value (in our example, the total profit). If you are interested in the detail of the algorithm, you shoud definitely watch this video.
The simplex algorithm is known to be a difficult problem in terms of complexity. While the base algorithm is EXPtime, it is generally very efficient in practice.
What Changed in 0.5 ?⚓
Among the main changes in this new version of ocplibsimplex:

Make the library's API more generic and easier to use (see the System Solving Example or the Linear Optimization Example);

All the modules are better documentated in their
.mli
interfaces (see coreSig.mli for example); 
the build system has been switched to
dune
We hope that this work of simplification will help you to integrate this library more easily in your projects!
If you want to follow this project, report an issue or contribute, you can find it on GitHub.
Please do not hesitate to contact us at OCamlPro: altergo@ocamlpro.com.
About AltErgo
AltErgo is an opensource automatic solver of mathematical formulas designed for program verification. AltErgo is very successful for proving formulas generated in the context of deductive program verification. It was originally designed and tuned to be used by the Why playform. Its development started in 2006 at the Laboratoire de Recherche en Informatique (LRI) of the Université Paris Sud and is maintained, developed and distributed since 2013 by the company OCamlPro.
AltErgo is part of the formal method team here at OCamlPro. This work is partially funded by the research projects Soprano, BWare, Vocal and LCHIP. If you like AltErgo, consider joining the AltErgo user’s Club
Most Recent Articles
2023
2022
2021
 Verification for Dummies: SMT and Induction
 Generating static and portable executables with OCaml
 opam 2.1.0 is released!
 opam 2.0.9 release
 Detecting identity functions in Flambda
 Détection de fonctions d’identité dans Flambda
 opam 2.1.0~rc2 released
 Tutorial: Format Module of OCaml
 Réunion annuelle du Club des utilisateurs d’AltErgo 2021
 New TryAltErgo