Nous sommes ravis d’annoncer la sortie officielle d’Alt-Ergo 2.6 ! Alt-Ergo est un démonstrateur automatisé développé par OCamlPro, largement utilisé en vérification formelle. Il joue un rôle clé dans les cadres d’analyse statique tels que le TIS Analyzer, SPARK et Frama-C. Cette nouvelle version introduit une série d’améliorations et de nouvelles fonctionnalités, en particulier dans le raisonnement sur les bit-vectors, la génération de modèles et l’optimisation. Les mises à jour d’Alt-Ergo 2.

Ce mardi 19 décembre 2023, tous les partenaires du projet Decysif (TrustInSoft, AdaCore, OCamlPro et l’équipe LMF) se sont réunis dans les locaux de TrustInSoft dans le 14ème arrondissement de Paris pour la réunion de lancement du projet ! Une bonne opportunité de revoir les objectifs ambitieux du projet, d’échanger entre les partenaires sur l’organisation et l’agenda des travaux. La réunion s’est terminée, comme souvent entre ces partenaires qui se connaissent bien, par des discussions techniques intenses, sur l’interaction entre Why3 (code source) et Alt-Ergo (code source), sur les cas d’usages pour tester Creusot (code source), ou encore sur les techniques de détection de failles en utilisant TIS Analyzer (code source de son Kernel libre) ou Spark (code source).