A contextual equivalence checker for IMJ*

We present coneqct: a contextual equivalence checking tool for terms of IMJ*, a fragment of Interface Middleweight Java for which the problem is decidable. Given two, possibly open (containing free identifiers), terms of the language, the contextual equivalence problem asks if the terms can be distinguished by any possible IMJ context. Although there has been a lot of prior work describing methods for constructing proofs of equivalence by hand, ours is the first tool to decide equivalences for a non-trivial, object-oriented language, completely automatically. This is achieved by reducing the equivalence problem to the emptiness problem for fresh-register pushdown automata. An evaluation demonstrates that our tool works well on examples taken from the literature