Ashesi Institutional Repository

Rodin Platform Why3 plug-in

Show simple item record Iliasov, Alexei Stankaitis, Paulius Adjepon-Yamoah, David Romanovsky, Alexander
dc.contributor.other Note: David Adjepon-Yamoah is a lecturer in Computer Science & Information Systems at Ashesi University 2019-01-23T16:50:57Z 2019-01-23T16:50:57Z 2016-05
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:
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.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
dc.description.version This is an author's pre-print

Files in this item

This item appears in the following Collection(s)

Show simple item record



My Account