Réunion annuelle du Club des utilisateurs d’Alt-Ergo 2021

---

La troisième réunion annuelle du Club des utilisateurs d’Alt-Ergo a eu lieu le 1er avril ! Cette réunion annuelle est l’endroit idéal pour passer en revue les besoins de chaque partenaire concernant Alt-Ergo. Nous avons eu le plaisir de recevoir nos partenaires pour discuter de la feuille de route concernant les développements et les améliorations futures d’Alt-Ergo.

Alt-Ergo est un démonstrateur automatique de formules mathématiques, créé au LRI et développé par OCamlPro depuis 2013. Pour en savoir plus ou rejoindre le Club, visitez le site https://alt-ergo.ocamlpro.com.

Notre Club a plusieurs objectifs. Son objectif principal est de garantir la pérennité d’Alt-Ergo en favorisant la collaboration entre les membres du Club et en tissant des liens avec les utilisateurs de méthodes formelles, telle que la communauté Why3. L’une de nos priorités est de définir les besoins des utilisateurs de solveurs de contraintes en étendant Alt-Ergo à de nouveaux domaines tels que le Model Checking, tout en concurrençant les autres solveurs de l’état de l’art au cours de compétitions internationales. Enfin, le dernier objectif du Club est de trouver de nouveaux projets ou contrats pour le développement de fonctionnalités à long terme.

Nous tenons à remercier tous nos membres pour leur soutien : Mitsubishi Electric R&D Centre Europe, AdaCore et le CEA List. Nous souhaitons également mettre en lumière l’équipe de développement Why3 avec laquelle nous travaillons pour améliorer nos outils.

Cette année, de nouveaux points d’intérêts ont été soulevés par nos membres. Dans un premier temps, la génération de modèles, ajoutée à Alt-Ergo suite à la dernière édition, a été utile à la majorité des membres du club. Les points techniques souhaités à présent sont de pouvoir raffiner les contraintes et étudier comment les propager. Dans un second temps a eu lieu la présentation de Dolmen, le parseur/typer qui permettra de ne typer qu’une seule fois les fichiers SMT2 et d’être prêt pour le SMT3. Son intégration à Alt-Ergo est en cours, l’avis des membres du club est enthousiaste sur les apports futurs de l’outil Dolmen à la communauté des solveurs SMT !

Ces fonctionnalités sont désormais nos principales priorités, retrouvez les planches présentées à la réunion du Club édition 2021. Pour suivre nos avancement et les nouveautés, n’hésitez pas à lire nos articles sur notre blog.

---

About Alt-Ergo

Alt-Ergo is an Open Source automatic solver of mathematical formulas designed for program verification. Alt-Ergo 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 Why3 platform. Its development started in 2006 at the Laboratoire de Recherche en Informatique (LRI - CNRS/Inria) of the Université Paris-Saclay and is maintained, developed and distributed since 2013 by the Formal Methods team at OCamlPro.

This work is made possible through research projects like Décysif, Soprano, BWare, Vocal and LCHIP, as well as support from our Alt-Ergo Users' Club members. If Alt-Ergo has been valuable to you, consider joining the Alt-Ergo Users' Club.