Rodin Platform Why3 plug-in
We brieﬂy present the motivation, architecture and usage experience as well as proof statistics for a new Rodin Platform proof back-end based on the Why3 umbrella prover. Why3 oﬀers a simple and versatile notation as a common interface to a large number of automated provers including all the leading SMT-LIB and TPTP compliant tools. The plug-in can function either in a local mode when all the provers are installed locally, or remotely as a cloud service. We discuss the experience of building the tool, the current status and the potential advantages of a cloud-hosted proof infrastructure.
Pre-print of a book chapter
Rodin Platform, Why3, cloud computing, theorem proving
Final publication is as follows: Iliasov A., Stankaitis P., Adjepon-Yamoah D., Romanovsky A. (2016) Rodin Platform Why3 Plug-In. In: Butler M., Schewe KD., Mashkoor A., Biro M. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2016. Lecture Notes in Computer Science, vol 9675. Springer, Cham