Alt-Ergo : Propulser la vérification de programmes par SMT pour l'industrie

Présentation

Alt-Ergo est un solveur SMT open source spécialisé dans la vérification déductive de programmes. Développé initialement vers 2006 au LRI (Université Paris-Saclay, Inria, CNRS) pour la plateforme Why3, il a été conçu pour gérer des conditions de vérification complexes avec une fiabilité et une précision extrêmes.

En 2013, l'équipe de méthodes formelles de Titagone a repris la maintenance, orientant le développement d'Alt-Ergo vers l'innovation, le support et l'intégration industrielle.

Le Défi

Le défi était ambitieux : fournir un solveur capable de gérer des théories logiques riches, des formules quantifiées et des constructions logicielles réelles (tableaux, enregistrements, vecteurs de bits, arithmétique flottante), tout en restant ouvert et performant. Titagone devait s'assurer qu'Alt-Ergo puisse servir de backend robuste pour une large gamme d'outils, incluant Why3, Frama-C, SPARK ou Atelier-B, répondant aux standards industriels de l'avionique et de la défense.

Pourquoi nous avoir choisis ?

La communauté académique et les partenaires industriels ont confié la gérance d'Alt-Ergo à Titagone en raison de notre position unique à l'interface entre recherche et industrie. Notre équipe combine une expertise profonde en méthodes formelles et en résolution SMT avec une expérience reconnue dans la maintenance d'infrastructures open source critiques. Notre collaboration étroite avec Inria a permis de poursuivre l'innovation d'Alt-Ergo tout en répondant aux exigences de certification industrielle.

Notre Approche

En partant de son architecture inspirée de la recherche, Titagone a étendu et affiné Alt-Ergo pour améliorer sa complétude et son automatisation.

Les innovations clés incluent une théorie native des vecteurs de bits (bit-vectors), la génération de modèles pour toutes les théories supportées, des objectifs d'optimisation et un support amélioré des nombres flottants. Ces développements ont permis à Alt-Ergo de s'attaquer à des problèmes de vérification industrielle combinant arithmétique complexe et manipulations de bas niveau.

Résultats

• 98 % de succès pour les preuves automatiques dans Atelier-B (contre ~84 % initialement).
• Conformité aux exigences de qualification avionique DO-178C.
• Adopté par Airbus, le CEA, Thales, AdaCore et TrustInSoft.
• Écosystème florissant avec une communauté d'utilisateurs et de R&D active.

Impact

Grâce à sa distribution open source et à un engagement actif, Titagone a transformé Alt-Ergo d'un prototype de recherche en un outil de haute assurance largement adopté. En combinant ingénierie logicielle rigoureuse et expertise scientifique, Alt-Ergo fait aujourd'hui le pont entre les avancées académiques et les besoins industriels concrets.