Résumé
Dans cet exposé, nous présentons la conception et des cas d'utilisation du démonstrateur automatique Alt-Ergo.
Alt-Ergo est un démonstrateur de la famille SMT spécialement conçu pour prouver la validité de formules logiques générées par des outils de vérification de programme comme Frama-C, Why3, Spark ou l'Atelier-B. Ces formules partagent toutes le même format : elles contiennent des déclarations de types de données, des axiomes pour définir des structures de données complexes, des modèles mémoires, des théories spécifiques (par ex. ensembles finis, flottants, vecteurs de bits) et enfin des obligations de preuve provenant de propriétés de programmes à vérifier.
Les choix de conception et d'implémentation d'Alt-Ergo ont tous été guidés pour traiter efficacement ce genre de formules. Ainsi, Alt-Ergo est le seul démonstrateur SMT qui permette de manipuler directement des formules écrites dans une logique du premier ordre avec des types polymorphes « à la ML ». Il dispose également de théories prédéfinies utiles à la preuve de programmes comme la théorie de l'égalité avec symboles non-interprétés, l'arithmétique sur les entiers et les réels, la théorie des tableaux fonctionnels polymorphes avec extensionalité, les types énumérés, les enregistrements et les symboles associatifs/commutatifs (AC).
Pour un traitement des formules avec quantificateurs, Alt-Ergo repose sur un SAT-solveur original couplé à une technique de mise en CNF « paresseuse », ainsi que sur algorithme de filtrage étendu pour manipuler des termes polymorphes. Son noyau met également en œuvre une méthode de combinaison de procédures de décision unique basée sur des techniques de réécriture qui lui permettent, par exemple, de traiter les symboles associatifs / commutatifs de manière efficace.
