Homer: A Higher-Order Observational Equivalence Model checkER

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 equivahanks 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 ch...

• Type: Conference
• Year: 2009
• Where: CAV
• Authors: David Hopkins, C.-H. Luke Ong
• Keywords: CAV 2009, Formal Methods, Model Checker, Observational-equivalence Model Checker, VPA Equivalence Problem