A user written application program goes through significant optimizing and parallelizing transformations, both (compiler) automated and human guided, before being mapped to an architecture. Formal verification of these transfor- mations is crucial to ensure that they preserve the original behavioural spec- ification. PRES+ model (Petri net based Representation of Embedded Sys- tems) encompassing data processing is used to model parallel behaviours more vividly. Being value based with a natural capability of capturing parallelism, PRES+ models depict such data dependencies more directly; accordingly, they are likely to be more convenient as the intermediate representations (IRs) of both source and transformed codes for translation validation than strictly se- quential, variable-based IRs like Finite State Machines with Data path (FS- MDs) (which are essentially sequential control and data flow graphs (CD- FGs)). This thesis presents two translation validation techniques for verify- ing optimizing and parallelizing code transformations by checking equivalence between two PRES+ models, one representing the source code and the other representing its optimized and (or) parallelized version.

Any path based (symbolic) program analysis method consists in introduc- ing cut-points in the loops so that each loop is cut in at least one cut-point; this step permits us to visualize any computation of a program as a sequence of fi- nite paths. Once computations are posed in terms of paths in the above manner, a path based equivalence checking strategy consists in finding equivalent paths in the models. Unlike sequential CDFG models like FSMDs, for PRES+ mod- els, such a sequence is expected to have parallel paths. It is, however, found that apparently cutting only the loops is not adequate to capture a computation as a sequence of parallel paths. The dissertation first describes a method of introducing cut-points so that a computation can be posed as a sequence of parallel paths. This method is referred to as dynamic cut-point induced path based equivalence checking "dynamic" because additional cut-points over and above those introduced to cut the loops are needed for the purpose and the method entails a symbolic execution of the model keeping track of the tokens and disregarding the symbolic values. Subsequently, we also reveal that it is possible to have a valid path based equivalence checking strategy even when the conventional approach of introducing cut-points only to cut the loops is followed. This method is referred to as static cut-point induced path based equivalence checking.

Correctness and complexity of the two methods have been treated formally. The methods have been implemented and tested and compared on several se- quential and parallel benchmarks. While underscoring the effectiveness of equivalence checking as a method for verification of machine independent op- timizing and parallelizing passes of compilers, the dissertation discusses some limitations of the work and identifies some future directions in which it can be enhanced.