Hobbit: A Tool for Contextual Equivalence Checking Using Bisimulation Up-to Techniques - Koutavas, Vasileios; Lin, Yu-Yang (My University, 2021)
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.
ML Family Workshop 2021
Keywords: Operational game semantics; Contextual equivalence; Bounded model checking; Symbolic bisimulation; Up-to techniques; BISIMULATION; computer science theory; contextual equivalence; model checking; operational game semantics; software verification