Rodin Platform Why3 plug-in
dc.contributor.author | Iliasov, Alexei | |
dc.contributor.author | Stankaitis, Paulius | |
dc.contributor.author | Adjepon-Yamoah, David | |
dc.contributor.author | Romanovsky, Alexander | |
dc.contributor.other | Note: David Adjepon-Yamoah is a lecturer in Computer Science & Information Systems at Ashesi University | |
dc.date.accessioned | 2019-01-23T16:50:57Z | |
dc.date.available | 2019-01-23T16:50:57Z | |
dc.date.issued | 2016-05 | |
dc.description.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. | en_US |
dc.description.sponsorship | Newcastle University (UK), School of Computing | |
dc.description.version | This is an author's pre-print | |
dc.identifier.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 | en_US |
dc.identifier.isbn | Final publication is a book with following ISBN: 978-3-319-33600-8 | |
dc.identifier.other | Final publication DOI is: https://doi.org/10.1007/978-3-319-33600-8_21 | |
dc.identifier.uri | http://hdl.handle.net/20.500.11988/402 | |
dc.language.iso | en | en_US |
dc.publisher | Springer, Cham | en_US |
dc.subject | Rodin Platform | en_US |
dc.subject | Why3 | |
dc.subject | cloud computing | |
dc.subject | theorem proving | |
dc.title | Rodin Platform Why3 plug-in | en_US |
dc.type | Pre-print of a book chapter | en_US |
Files
Original bundle
1 - 1 of 1
Loading...
- 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: