Cut-Bisimulation and Program Equivalence

We propose an algorithmic semantics-based approach for proving equivalence of programs written in possibly different languages. We introduce a new notion of bisimulation, named cut-bisimulation, that allows the two programs to semantically synchronize at relevant “cut” points, but to evolve independently otherwise. While being analogous, cut-bisimulation is different from stuttering bisimulation. We provide realistic counter-example programs that are cut-bisimilar but not stuttering-bisimilar, which can be easily found in a compiler optimization. Also, we identify a subclass of stuttering bisimulation that can be reduced to cut-bisimulation. Based on cut-bisimulation, we have implemented the first language-independent tool for proving program equivalence, parametric in the formal semantics of the source and target languages, built on top of the K framework. As a preliminary evaluation, we instantiated our tool with an LLVM semantics, and used it to prove equivalence of the aforementioned example programs written in LLVM.