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

Auteurs: OCamlPro
Date: 2021-04-29
Catégorie: Formal Methods
Tags: alt-ergo, fr



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 vérificateur automatique de formules mathématiques, développé conjointement par le LRI et OCamlPro (depuis 2014). 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 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.

Alt-Ergo 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 Alt-Ergo Users' Club members. If you like Alt-Ergo, consider joining the Alt-Ergo user’s Club.