Towards Generating SPARK from Event-B Models. - Sanjeevan Sritharan; Thai Son Hoang (IFM, 2020)