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.
Iliasov, A , Stankaitis, P , Adjepon-Yamoah, D & Romanovsky, A (2021). Rodin Platform Why3 plug-in.. Afribary. Retrieved from https://tracking.afribary.com/works/rodin-platform-why3-plug-in-1
Iliasov, Alexei et. al. "Rodin Platform Why3 plug-in." Afribary. Afribary, 26 Mar. 2021, https://tracking.afribary.com/works/rodin-platform-why3-plug-in-1. Accessed 23 Nov. 2024.
Iliasov, Alexei, Paulius Stankaitis , David Adjepon-Yamoah and Alexander Romanovsky . "Rodin Platform Why3 plug-in.". Afribary, Afribary, 26 Mar. 2021. Web. 23 Nov. 2024. < https://tracking.afribary.com/works/rodin-platform-why3-plug-in-1 >.
Iliasov, Alexei , Stankaitis, Paulius , Adjepon-Yamoah, David and Romanovsky, Alexander . "Rodin Platform Why3 plug-in." Afribary (2021). Accessed November 23, 2024. https://tracking.afribary.com/works/rodin-platform-why3-plug-in-1