The Application of Formal Methods to the Reverse Engineering of Imperative Program Code

Formal methods in software development provide many benefits in the forward engineering aspect of software development. One of the advantages of using formal methods in software development is that the formal notations are precise, verifiable, and facilitate automated processing. Reverse engineering is the process of constructing high level representations from lower level instantiations of an existing system. There are two main objectives that the research described in this thesis covers. First, a new approach to the construction of formal specifications from program code has been developed. To this end, a propagational model of translation has been developed that ..