Deriving bisimulation relations from path based equivalence checkers

Translation validation is an undecidable problem. Bisimulation relation based approaches, nevertheless, have been widely successful in translation validation of programs albeit with some drawbacks. These drawbacks include non-termination of the verification methodology and significant restrictions on the structures of programs to be checked for equivalence. We have developed a path based equivalence checker which propagates mismatched values over consecutive paths to alleviate these drawbacks. In this work, we show how a bisimulation relation between a program and its translated version can be constructed from the outputs of such a value propagation based equivalence checker. Moreover, none of the earlier methods that establish equivalence through construction of bisimulation relations has been shown to tackle code motions across loops; the present work demonstrates, for the first time, the existence of a bisimulation relation under such a situation.