Event-B and Cloud Provers

Abstract

We discuss the whys and hows of remotely managing a collection of automated theorem provers supporting verification of Event-B models in the Rodin Platform[5]. We report on the current state of the work, our general aspirations and a range of technical obstacles encountered so far.

Description

Event-B, Rodin Platform, Theorem Proving, Cloud Computing, Proof Obligation

Keywords

Event-B, Rodin Platform, theorem proving, cloud computing, proof obligation

Citation

Preprint of paper from Sorge, Volker. 2015. Proceedings of the Automated Reasoning Workshop 2015 Bridging the Gap between Theory and Practice ARW 2015 9th-10th April 2015 School of Computer Science University of Birmingham Birmingham

DOI