Sortie d'Alt-Ergo 2.6 : Renforcer la vérification formelle avec de nouvelles fonctionnalités

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.6 sont directement liées aux avancées réalisées dans le cadre du projet de recherche DéCySif qui réunit AdaCore, Inria, OCamlPro et TrustInSoft.

Quoi de neuf ?

  • Support amélioré des bit-vectors et des types de données algébriques.
  • Nouvelles capacités d’optimisation pour guider le comportement du démonstrateur.
  • Génération de modèles pour un éventail plus large de théories, y compris les bit-vectors.

Ces améliorations sont particulièrement utiles pour ceux qui travaillent sur la vérification de code bas-niveau, la cryptographie ou le débogage de systèmes complexes.

Pour en savoir plus sur cette version, y compris les comparaisons de performances et les autres fonctionnalités, consultez les notes de version complètes sur le Blog d’OCamlPro.

Ne manquez pas cette mise à jour puissante d’Alt-Ergo !