From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques - Koutavas, Vasileios (Springer, 2022)
We present a bounded equivalence verification technique for higher-order programs with local state. This technique combines fully abstract symbolic environmental bisimulations similar to symbolic game semantics, novel up-to techniques, and lightweight state invariant annotations. This yields an equivalence verification technique with no false positives or negatives. The technique is bounded-complete, in that all inequivalences are automatically detected given large enough bounds. Moreover, several hard equivalences are proved automatically or after being annotated with state invariants. We realise the technique in a tool prototype called Hobbit and benchmark it with an extensive set of new and existing examples. Hobbit can prove many classical equivalences including all Meyer and Sieber examples.
LNCS
28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (ETAPS 2020)
PUBLISHED
Munich, Germany
Keywords: Contextual equivalence; Bounded model checking; Symbolic bisimulation; Up-to techniques; Operational game semantics; BISIMULATION; Formal Semantics; contextual equivalence; model checking; operational game semantics; programming language theory; software verification