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 dependency graph-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.

• cses95.ps