Rodin Platform Why3 plug-in

Abstract

We briefly 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 offers 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.

Description

Keywords

Rodin Platform, Why3, cloud computing, theorem proving

Citation

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

DOI