From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques

Vasileios Koutavas, Yu-Yang Lin, Nikos Tzevelekos

We present a bounded equivalence verification technique for higher-order programs with local state. This technique combines fully abstract symbolic environmental bisimulations simi…