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