ProB and Jupyter for Logic, Set Theory, Theoretical Computer Science and Formal Methods

Abstract

We present a tool for using the B language in computational notebooks, based on the Jupyter Notebook interface and the ProB tool. Applications of B notebooks include executable documentation of formal models, interactive manuals, validation reports but also teaching of formal methods, logic, set theory and theoretical computer science. In addition to B and Event-B, the tool supports Z, (\textsc {TLA}^{+}) and Alloy.

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{GelessusL20,
  author       = {David Gele{\ss}us and
                  Michael Leuschel},
  editor       = {Alexander Raschke and
                  Dominique M{\'{e}}ry and
                  Frank Houdek},
  title        = {ProB and Jupyter for Logic, Set Theory, Theoretical Computer Science
                  and Formal Methods},
  booktitle    = {Rigorous State-Based Methods - 7th International Conference, {ABZ}
                  2020, Ulm, Germany, May 27-29, 2020, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {12071},
  pages        = {248--254},
  publisher    = {Springer},
  year         = {2020},
  url          = {https://doi.org/10.1007/978-3-030-48077-6\_19},
  doi          = {10.1007/978-3-030-48077-6\_19},
  timestamp    = {Tue, 16 Jun 2020 17:18:07 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/GelessusL20.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}