Browsing by Author "Romanovsky, Alexander"
Now showing 1 - 1 of 1
Results Per Page
Sort Options
Item Rodin Platform Why3 plug-in(Springer, Cham, 2016-05) Iliasov, Alexei; Stankaitis, Paulius; Adjepon-Yamoah, David; Romanovsky, Alexander; Note: David Adjepon-Yamoah is a lecturer in Computer Science & Information Systems at Ashesi UniversityWe 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.