Discharging Proof Obligations from Atelier B using Multiple Automated Provers

David Mentré 1, * Claude Marché 2, 3 Jean-Christophe Filliâtre 2, 3 Masashi Asuka 4
* Auteur correspondant
3 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : We present a method to discharge proof obligations from Atelier B using multiple SMT solvers. It is based on a faithful modeling of B's set theory into polymorphic first-order logic. We report on two case studies demonstrating a significant improvement in the ratio of obligations that are automatically discharged.
Type de document :
Communication dans un congrès
Steve Reeves and Elvinia Riccobene. ABZ - 3rd International Conference on Abstract State Machines, Alloy, B and Z, Jun 2012, Pisa, Italy. Springer, 2012
Liste complète des métadonnées

https://hal.inria.fr/hal-00681781
Contributeur : Claude Marché <>
Soumis le : jeudi 22 mars 2012 - 14:02:29
Dernière modification le : jeudi 9 février 2017 - 15:52:41
Document(s) archivé(s) le : lundi 26 novembre 2012 - 11:55:44

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00681781, version 1

Collections

Citation

David Mentré, Claude Marché, Jean-Christophe Filliâtre, Masashi Asuka. Discharging Proof Obligations from Atelier B using Multiple Automated Provers. Steve Reeves and Elvinia Riccobene. ABZ - 3rd International Conference on Abstract State Machines, Alloy, B and Z, Jun 2012, Pisa, Italy. Springer, 2012. <hal-00681781>

Partager

Métriques

Consultations de
la notice

692

Téléchargements du document

256