Deriving bisimulation relations from path based equivalence checkers
Kunal Banerjee, Dipankar Sarkar, Chittaranjan Mandal · Formal Aspects of Computing · 2016
Abstract 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.