Hobbit: A Tool for Contextual Equivalence Checking Using Bisimulation Up-to Techniques

Abstract

We present a bounded equivalence verification tool called Hobbit for higher-order programs with local state—based on a subset of OCaml—that combines fully abstract symbolic environmental bisimulations, novel up-to techniques, and lightweight invariant annotations. The tool reports no false positives or negatives, can automatically detect all inequivalences, and is able to automatically or semi-automatically prove many equivalences, including all classical Meyer and Sieber equivalences.