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

Authors: Aurore Dromby
Date: 2020-03-03
Category: Formal Methods
Tags: alt-ergo, fr



Alt-Ergo meeting Logo Alt-Ergo

La deuxième réunion annuelle du Club des utilisateurs d’Alt-Ergo a eu lieu à la mi-février ! Notre réunion annuelle est l’endroit idéal pour passer en revue les besoins de chaque partenaire concernant Alt-Ergo. Cette année, 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, le premier étant de garantir la pérennité d’Alt-Ergo en favorisant la collaboration entre les membres du Club et en renforçant la collaboration avec les communautés de méthodes formelles telles que Why3. L’une de nos priorités est d’augmenter le nombre d’utilisateurs de notre outil en l’étendant à de nouveaux domaines tels que le Model Checking, la participation à des compétitions internationales étant également un moyen de gagner en visibilité. Enfin, le dernier objectif du Club est de trouver de nouveaux projets ou contrats pour le développement de fonctionnalités à long terme.

Nous remercions tous nos membres pour leur soutien et souhaitons la bienvenue à Mitsubishi Electric R&D Centre Europe qui rejoint AdaCore et le CEA List en tant que membre du Club cette année. Nous souhaitons également mettre en lumière l’équipe de développement Why3 avec laquelle nous travaillons pour améliorer nos outils.

Nos membres sont particulièrement intéressés par les points suivants :

– Une meilleure génération de modèles et de contre-exemples

– L’ajout de la théorie des séquences

– L’amélioration du support de l’arithmétique non linéaire dans Alt-Ergo

Ces fonctionnalités sont maintenant nos principales priorités. Pour suivre nos avancement et les nouveautés, n’hésitez pas à lire nos articles sur ce 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.