Program transformation using temporal logic specifications. - D. J. Lacey (2003)