Murali, R.; Ireland, A. E-SPARK: Automated Generation of Provably Correct Code from Formally Verified Designs. eceasst 2012, 53.