Tuning the Alt-Ergo SMT Solver for B Proof Obligations

Sylvain Conchon 1, 2 Mohamed Iguernelala 3
1 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 : In this paper, we present recent developments on the Alt-Ergo SMT-solver to efficiently discharge proof obligations (PO) generated by Atelier B. This includes a new plugin architecture to facilitate experiments with different SAT engines, new heuristics to handle quantified formulas, and important modifications in its internal data structures to boost performances of core decision procedures. Benchmarks realized on more than 10,000 PO generated from industrial B projects show significant improvements.
Type de document :
Communication dans un congrès
ABZ, Jun 2014, Toulouse, France. 2014
Liste complète des métadonnées


https://hal.inria.fr/hal-01093000
Contributeur : Sylvain Conchon <>
Soumis le : mardi 9 décembre 2014 - 22:02:19
Dernière modification le : jeudi 9 février 2017 - 15:03:38
Document(s) archivé(s) le : mardi 10 mars 2015 - 12:30:12

Fichier

alt-ergo.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01093000, version 1

Citation

Sylvain Conchon, Mohamed Iguernelala. Tuning the Alt-Ergo SMT Solver for B Proof Obligations. ABZ, Jun 2014, Toulouse, France. 2014. <hal-01093000>

Partager

Métriques

Consultations de
la notice

114

Téléchargements du document

83