The EventB2Dafny Tool. EventB2Dafny is implemented as a plug-in of Rodin. It takes an EventB machine proof-obligation and generates an equivalent Dafny program. You can then use Dafny proof environment to discharge the proof-obligation. You can check on the syntax of Dafny programs here

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 1 article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Dalvandi, Mohammadsadegh; Butler, Michael; Rezazadeh, Abdolbaghi: From Event-B models to Dafny code contracts (2015)