Browsing by Author "Stankaitis, Paulius"

Filter results by typing the first few letters
Now showing 1 - 2 of 2
  • Thumbnail Image
    ItemOpen Access
    Event-B and Cloud Provers
    (Final publisher: University of Birmingham, 2015-04) Iliasov, Alexei; Stankaitis, Paulius; Adjepon-Yamoah, David Ebo
    We discuss the whys and hows of remotely managing a collection of automated theorem provers supporting verification of Event-B models in the Rodin Platform[5]. We report on the current state of the work, our general aspirations and a range of technical obstacles encountered so far.
  • Thumbnail Image
    ItemOpen Access
    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 University
    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.