Formal Verification of Transformations on Dependency Graphs in Optimizing Compilers

Dependency graphs are used as intermediate representations in optimizing compilers and software-engineering. In a transformational design approach, optimization and refinement transformations are used to transform dependencygraph -based specifications at higher abstraction levels to those at lower abstraction levels. An informal representation would lead to subtle errors, making it difficult to guarantee the correctness of the transformations. In this work, we investigated the formal specification and efficient mechanical verification of transformations on dependency graphs. 1 Introduction Dependency graphs 1 are used to model model data and control flow in software and hardware design. A dependency graph consists of nodes representing operations or processes, and directed edges representing data dependencies and data flow through the system. In addition, control flow could also be represented in a dependency graph in several ways. We show an example of such a graph in Figure 1. In ..