Ward, M. (2004) Pigs from Sausages? Reengineering from Assembler to C via Fermat Transformations. Science of Computer Programming, Special Issue on Program Transformation, 52, 213-255. http://www.gkc.org.uk/martin/papers/migration-t.pdf

has been cited by the following article:

• TITLE: A Logical Treatment of Non-Termination and Program Behaviour

  AUTHORS: Martin Ward, Hussein Zedan

  KEYWORDS: Formal Methods, Refinement, Non-Termination, Non-Determinism, Weakest Precondition, Temporal Logic, Wide-Spectrum Language

  JOURNAL NAME: Journal of Software Engineering and Applications, Vol.7 No.7, June 5, 2014

  ABSTRACT: Can the semantics of a program be represented as a single formula? We show that one formula is insufficient to handle assertions, refinement or slicing, while two formulae are sufficient: A (S) , defining non-termination, and B (S), defining behaviour. Any two formulae A and B will define a corresponding program. Refinement is defined as implication between these formulae.