M. Dalvandi, M. Butler, and A. Rezazadeh, “Transforming Event-B Models to Dafny Contracts”, eceasst, vol. 72, Nov. 2015.