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
References in zbMATH (referenced in 2 articles )
Showing results 1 to 2 of 2.
- Dalvandi, Mohammadsadegh; Butler, Michael; Rezazadeh, Abdolbaghi: From Event-B models to Dafny code contracts (2015)
- Dastani, Mehdi (ed.); Sirjani, Marjan (ed.): Fundamentals of software engineering. 6th international conference, FSEN 2015, Tehran, Iran, April 22--24, 2015. Revised selected papers (2015)