Title :
The EventB2Dafny Rodin plug-in
Author :
Cataño, Néstor ; Leino, K. Rustan M ; Rivera, Víctor
Author_Institution :
Univ. of Madeira, Funchal, Portugal
Abstract :
This paper presents a translation of Rodin proof-obligations into the input language of Dafny, and the implementation of the translation as the EventB2Dafny Rodin plug-in. Rodin is a platform that provides support for Event-B. The paper uses a simplified Event-B model for social-networking to illustrate the translation and to describe the generated Dafny model. EventB2Dafny supports the full Event-B syntax and its full source code is available online.
Keywords :
formal verification; refinement calculus; theorem proving; Dafny model; Event-B model; EventB2Dafny Rodin plug-in; Rodin proof-obligation; social-networking; Abstracts; Calculus; Computer languages; Concrete; Context; Social network services; Syntactics; Boogie; Dafny; Event-B; Proof Obligations; Refinement Calculus; Rodin;
Conference_Titel :
Developing Tools as Plug-ins (TOPI), 2012 2nd Workshop on
Conference_Location :
Zurich
Print_ISBN :
978-1-4673-1819-8
DOI :
10.1109/TOPI.2012.6229810
