Introducing Inductive Construction in B with the Theory Plugin

Julien Cervelle, Frédéric Gervais
Digital Printed Abstract View Cite
Type
Conference paper
Publication
9th International Conference on Rigorous State Based Methods (ABZ'23)

Abstract

Proving theorems and properties on B models, recursively-defined functions is a convenient tool which is missing in B proofs. The main contribution of this paper is the definition of a new theory without new concrete types and without axioms to enable the use of constructions by induction; This theory has been specified and proved within the Theory Plugin in Rodin. This induction theory clearly improves the existing B prover. This is illustrated in this paper by the implementation of ZFC in the Theory Plugin.

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{CervelleG23,
  author       = {Julien Cervelle and
                  Fr{\'{e}}d{\'{e}}ric Gervais},
  editor       = {Uwe Gl{\"{a}}sser and
                  Jos{\'{e}} Creissac Campos and
                  Dominique M{\'{e}}ry and
                  Philippe A. Palanque},
  title        = {Introducing Inductive Construction in {B} with the Theory Plugin},
  booktitle    = {Rigorous State-Based Methods - 9th International Conference, {ABZ}
                  2023, Nancy, France, May 30 - June 2, 2023, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {14010},
  pages        = {43--58},
  publisher    = {Springer},
  year         = {2023},
  url          = {https://doi.org/10.1007/978-3-031-33163-3\_4},
  doi          = {10.1007/978-3-031-33163-3\_4},
  timestamp    = {Fri, 02 Jun 2023 21:23:53 +0200},
  biburl       = {https://dblp.org/rec/conf/zum/CervelleG23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'23

Related