The EventB2Dafny rodin plug-in

Néstor Cataño,K. Rustan M. Leino,Víctor Rivera

TOPI@ICSE（2012）

引用 22|浏览12

暂无评分

摘要

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.

查看译文

关键词

formal verification,refinement calculus,theorem proving,Dafny model,Event-B model,EventB2Dafny Rodin plug-in,Rodin proof-obligation,social-networking,Boogie,Dafny,Event-B,Proof Obligations,Refinement Calculus,Rodin,

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要