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