Discharging Proof Obligations from Atelier B Using Multiple Automated Provers

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

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{MentreMFA12,
  author       = {David Mentr{\'{e}} and
                  Claude March{\'{e}} and
                  Jean{-}Christophe Filli{\^{a}}tre and
                  Masashi Asuka},
  editor       = {John Derrick and
                  John S. Fitzgerald and
                  Stefania Gnesi and
                  Sarfraz Khurshid and
                  Michael Leuschel and
                  Steve Reeves and
                  Elvinia Riccobene},
  title        = {Discharging Proof Obligations from Atelier {B} Using Multiple Automated
                  Provers},
  booktitle    = {Abstract State Machines, Alloy, B, VDM, and {Z} - Third International
                  Conference, {ABZ} 2012, Pisa, Italy, June 18-21, 2012. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {7316},
  pages        = {238--251},
  publisher    = {Springer},
  year         = {2012},
  url          = {https://doi.org/10.1007/978-3-642-30885-7\_17},
  doi          = {10.1007/978-3-642-30885-7\_17},
  timestamp    = {Sun, 02 Jun 2019 21:23:59 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/MentreMFA12.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}