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 platform. 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 methods team here at OCamlPro. This work is partially funded by the research projects Soprano, BWare, Vocal and LCHIP and the AltErgo Users' Club members. If you like AltErgo, consider joining the AltErgo user’s Club.
Articles les plus récents
2024
 opam 2.2.0 release!
 Flambda2 Ep. 2: Loopifying TailRecursive Functions
 Fixing and Optimizing the GnuCOBOL Preprocessor
 OCaml Backtraces on Uncaught Exceptions
 Opam 102: Pinning Packages
 Flambda2 Ep. 1: Foundational Design Decisions
 Behind the Scenes of the OCaml Optimising Compiler Flambda2: Introduction and Roadmap
 Lean 4: When Sound Programs become a Choice
 Opam 101: The First Steps
2023
 Maturing LearnOCaml to version 1.0: Gateway to the OCaml World
 The latest release of AltErgo version 2.5.1 is out, with improved SMTLIB and bitvector support!
 2022 at OCamlPro
 Autofonce, GNU Autotests Revisited
 Subsingleinstruction Peano to machine integer conversion
 Statically guaranteeing security properties on Java bytecode: Paper presentation at VMCAI 23
 Release of ocplibsimplex, version 0.5
 The Growth of the OCaml Distribution
2022