The Alt-Ergo Users' Club
The Alt-Ergo Automatic SMT-based Theroem Prover was born in 2006 at LRI, INRIA Saclay and CNRS, and has been maintained by OCamlPro since 2013. Alt-Ergo is tuned to prove properties generated for program verification, especially by the Why3 deductive framework.
This automatic solver of mathematical formulas is based on Satisfiability Modulo Theories (SMT). Solvers of this family have made impressive advances and became very popular during the last decade. They are now used is various domains such as hardware design, software verification and formal testing.
In 2019, OCamlPro has created the Alt-Ergo Users' Club, with the goal to gather some of the big users of Alt-Ergo to fund its maintainance and evolution.
Members of the Club get the right to influence the development roadmap of Alt-Ergo, get access to discussion forums between advanced users and developers of Alt-Ergo, and get access to an open-source licence on the latest version of Alt-Ergo (see Services to Members for more information).
Current Members
Join our current members!
In 2025, the Alt-Ergo Users' Club will be including the following Gold members AdaCore, CEA, Trust In Soft, Thalès, and Bronze Member MERCE (Mitsubishi Electric R&D Europe). Our long term partners of the Inria/CNRS research team Why3 shepherded by Claude Marché is an invited member.
Services to Members
Depending on their level of sponsorsing, members are given a set of services to help them take benefit of all features of Alt-Ergo:
- Chat between Members, to share and discuss features and usage of Alt-Ergo;
- Yearly meeting in the offices of OCamlPro;
- Access to the latest version of Alt-Ergo for commercial use;
- Logos displayed on websites;
- Days of responsiveness in case of critical problem;
- Voting rights on important decisions;
Levels of Sponsorships
