A suite of tools for facilitating reverse engineering using formal methods

As a program evolves, it becomes increasingly difficult to understand and reason about changes in source code. Eventually if enough changes are made without a corresponding modification of the software documentation, reverse engineering and design recovery techniques must be used in order to understand the current behavior of a system. In our previous investigations, we described a formal technique for reverse engineering. One of the benefits of formal techniques is that they are amenable to automated processing. In this paper, we describe an integrated suite of tools that we have developed to support reverse engineering and analysis of C programs.