E-SPARK: Automated Generation of Provably Correct Code from Formally Verified Designs. - Rajiv Murali; Andrew Ireland (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2012)

A Rigorous Approach to Combining Use Case Modelling and Accident Scenarios. - Rajiv Murali; Andrew Ireland; Gudmund Grov (NFM, 2015)

UC-B: Use Case Modelling with Event-B. - Rajiv Murali; Andrew Ireland; Gudmund Grov (ABZ, 2016)