We present  Homer  , an observational-equivalence model checker for the 3rd-order fragment of Idealized Algol (IA) augmented with iteration. It works by first translating terms of the fragment into a precise representation of their game semantics as visibly pushdown automata (VPA). The VPA-translates are then passed to a VPA toolkit (which we have implemented) to test for equivalence. Thanks to the fully abstract game semantics, observational equivalence of these IA-terms reduces to the VPA Equivalence Problem. Our checker is thus sound and complete; because it model checks  open  terms, our approach is also compositional. Further, if the terms are inequivalent,  Homer  will produce both a game-semantic and an operational-semantic counter-example, in the form of a play and a separating context respectively. We showcase these features on a number of examples and (where appropriate) compare its performance with similar tools. To the best of our knowledge,  Homer  is the first implementation of a model checker of 3rd-order programs.
['David Hopkins', 'Chi-Keong Ong']
Homer: A Higher-Order Observational Equivalence Model checkER