Discharging Proof Obligations from Atelier B using Multiple Automated Provers - INRIA - Institut National de Recherche en Informatique et en Automatique Accéder directement au contenu
Communication Dans Un Congrès Année : 2012

Discharging Proof Obligations from Atelier B using Multiple Automated Provers

Résumé

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.

Domaines

Logique en informatique [cs.LO]
Fichier principal
Vignette du fichier
main.pdf (388.34 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Claude Marché  : Connectez-vous pour contacter le contributeur

https://inria.hal.science/hal-00681781

Soumis le : jeudi 22 mars 2012-14:02:29

Dernière modification le : samedi 10 février 2024-03:07:49

Archivage à long terme le : lundi 26 novembre 2012-11:55:44

Télécharger pour visualiser

Dates et versions

hal-00681781 , version 1 (22-03-2012)

Identifiants

  • HAL Id : hal-00681781 , version 1

Citer

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

Exporter

BibTeX XML-TEI Dublin Core DC Terms EndNote DataCite

Collections

EC-PARIS CNRS INRIA UMR8623 INRIA2 UNIV-PARIS-SACLAY ANR
1219 Consultations
329 Téléchargements

Partager

Gmail Facebook X LinkedIn More