Alt-Ergo 2.2

Sylvain Conchon 1, 2 Albin Coquereau 3, 1 Mohamed Iguernlala 4, 1 Alain Mebsout 4
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : Alt-Ergo is an SMT solver jointly developed by Université Paris-Sud and the OCamlPro company. The first version was released in 2006. Since then, its architecture has been continuously adapted for proving formulas generated by software development frameworks. As type systems with polymorphism arise naturally is such platforms, the design of Alt-Ergo has been guided (and constrained) by a native-and non SMT-LIB compliant-input language for a polymorphic first-order logic. In this paper, we present the last version of Alt-Ergo, its architecture and main features. The main recent work is a support for a conservative polymorphic extension of the SMT-LIB 2 standard. We measure Alt-Ergo's performances with this new frontend on a set of benchmarks coming from the deductive program verification systems Frama-C, SPARK 2014, Why3 and Atelier-B, as well as from the SMT-LIB benchmarks library.
Type de document :
Communication dans un congrès
SMT Workshop: International Workshop on Satisfiability Modulo Theories, Jul 2018, Oxford, United Kingdom. 2018, 〈http://smt-workshop.cs.uiowa.edu/2018/〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01960203
Contributeur : Mohamed Iguernlala <>
Soumis le : mercredi 9 janvier 2019 - 12:15:03
Dernière modification le : jeudi 7 février 2019 - 15:28:13

Fichier

Alt-Ergo-2.2--SMT-Workshop-201...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01960203, version 1

Citation

Sylvain Conchon, Albin Coquereau, Mohamed Iguernlala, Alain Mebsout. Alt-Ergo 2.2. SMT Workshop: International Workshop on Satisfiability Modulo Theories, Jul 2018, Oxford, United Kingdom. 2018, 〈http://smt-workshop.cs.uiowa.edu/2018/〉. 〈hal-01960203〉

Partager

Métriques

Consultations de la notice

182

Téléchargements de fichiers

38