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.
CITATION STYLE
Koutavas, V., Lin, Y. Y., & Tzevelekos, N. (2022). From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 13244 LNCS, pp. 178–195). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-99527-0_10
Mendeley helps you to discover research relevant for your work.