Rodin Platform Why3 plug-in

dc.contributor.authorIliasov, Alexei
dc.contributor.authorStankaitis, Paulius
dc.contributor.authorAdjepon-Yamoah, David
dc.contributor.authorRomanovsky, Alexander
dc.contributor.otherNote: David Adjepon-Yamoah is a lecturer in Computer Science & Information Systems at Ashesi University
dc.date.accessioned2019-01-23T16:50:57Z
dc.date.available2019-01-23T16:50:57Z
dc.date.issued2016-05
dc.description.abstractWe 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.en_US
dc.description.sponsorshipNewcastle University (UK), School of Computing
dc.description.versionThis is an author's pre-print
dc.identifier.citationFinal 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, Chamen_US
dc.identifier.isbnFinal publication is a book with following ISBN: 978-3-319-33600-8
dc.identifier.otherFinal publication DOI is: https://doi.org/10.1007/978-3-319-33600-8_21
dc.identifier.urihttp://hdl.handle.net/20.500.11988/402
dc.language.isoenen_US
dc.publisherSpringer, Chamen_US
dc.subjectRodin Platformen_US
dc.subjectWhy3
dc.subjectcloud computing
dc.subjecttheorem proving
dc.titleRodin Platform Why3 plug-inen_US
dc.typePre-print of a book chapteren_US

Files

Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
Iliasov_A, Stankaitis_P, Adjepon-Yamoah_D and Romanovsky_A_2016_Rodin Platform Why3 plug-in.pdf
Size:
247.61 KB
Format:
Adobe Portable Document Format
Description: