Skip to Main content Skip to Navigation
New interface
Conference papers

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 
* Corresponding author
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.
Document type :
Conference papers
Complete list of metadata
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Thursday, March 22, 2012 - 2:02:29 PM
Last modification on : Tuesday, July 5, 2022 - 9:31:40 AM
Long-term archiving on: : Monday, November 26, 2012 - 11:55:44 AM


Files produced by the author(s)


  • HAL Id : hal-00681781, version 1



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⟩



Record views


Files downloads