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

TL;DR

This paper introduces a bounded equivalence verification method for higher-order programs with local state, combining symbolic bisimulations, novel up-to techniques, and lightweight invariants, implemented in the Hobbit tool.

Contribution

It presents a new bounded verification technique that is complete and can automatically prove many classical program equivalences, including complex examples.

Findings

Hobbit successfully proves many classical equivalences.

The technique detects all inequivalences with sufficient bounds.

Several hard equivalences are proved automatically or with invariants.

Abstract

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.