For most high level languages, two procedures are equivalent
if they transform a pair of isomorphic stores to isomorphic stores. How-
ever, tools for modular checking of such equivalence impose a stronger
check where isomorphism is strengthened to equality of stores. This re-
sults in the inability to prove many interesting program pairs with re-
cursion and dynamic memory allocation.
In this work, we present RIE, a methodology to modularly establish
equivalence of procedures in the presence of memory allocation, cyclic
data structures and recursion. Our technique addresses the need for find-
ing witnesses to isomorphism with angelic allocation, supports reasoning
about equivalent procedures calls when the stores are only locally iso-
morphic, and reasoning about changes in the order of procedure calls.
We have implemented RIE by encoding it in the Boogie program verifier.
We describe the encoding and prove its soundness.