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 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.
Keywords for this software
References in zbMATH (referenced in 4 articles )
Showing results 1 to 4 of 4.
- Broadbent, Christopher; Carayol, Arnaud; Hague, Matthew; Serre, Olivier: C-SHORe: a collapsible approach to higher-order verification (2013)
- Hopkins, David; Murawski, Andrzej S.; Ong, C.-H.Luke: A fragment of ML decidable by visibly pushdown automata (2011)
- Bakewell, Adam; Dimovski, Aleksandar; Ghica, Dan R.; Lazić, Ranko: Data-abstraction refinement: a game semantic approach (2010)
- Dimovski, Aleksandar; Ghica, Dan R.; Lazić, Ranko: Data-abstraction refinement: A game semantic approach (2005)