R. Murali and A. Ireland, “E-SPARK: Automated Generation of Provably Correct Code from Formally Verified Designs”, eceasst, vol. 53, Dec. 2012.