The second annual meeting of the Alt-Ergo Users’ Club was held in mid-February. Our annual meeting is the perfect place to review each partner’s needs regarding Alt-Ergo. This year, we had the pleasure of receiving our partners to discuss the roadmap for future Alt-Ergo developments and enhancements.
Alt-Ergo is an automatic mathematical formula checker, jointly developed by LRI and OCamlPro (since 2014). For more information or to join the club, visit https://alt-ergo.ocamlpro.com.
Our club has several goals, the first of which is to ensure the sustainability of Alt-Ergo by fostering collaboration among club members and strengthening collaboration with formal method communities such as Why3. One of our priorities is to increase our user community by extending our tool to new sectors such as Model Checking. Participation in international competitions is also a way to gain visibility. Finally, the last objective of the club is to find new projects or contracts for the development of long-term functionalities.
We thank all our members for their support and bid a warm welcome Mitsubishi Electric R&D Centre Europe as they join AdaCore and the CEA list as a member of the club this year. We would also like to highlight the Why3 development team with whom we are working to improve our tools.
Our members are particularly interested in:
- Better generation of models and counter-examples.
- The addition of sequence theory.
- The improvement of non-linear arithmetic support in Alt-Ergo.
These features are now top priorities for us. For more information, you can read our articles on this blog.
This entry was posted in Blog and tagged Alt-Ergo. Bookmark the permalink.
Originally published at http://www.ocamlpro.com on March 3, 2020.
