@TechReport{      salvati:hal-00741077,
  Author        = "Salvati, Sylvain and Walukiewicz, Igor",
  Abstract      = "{We propose a model-based approach to the model checking problem for recursive schemes. Since simply typed lambda calculus with the fixpoint operator, lambda-Y-calculus, is equivalent to schemes, we propose to use a model of lambda-Y to discriminate the terms that satisfy a given property. If a model is finite in every type, this gives a decision procedure. We provide a construction of such a model for every property expressed by automata with trivial acceptance conditions and divergence testing. We argue that having a model capable of recognizing terms satisfying a given property has other benefits than just providing decidability of the model-checking problem. We show a very simple construction transforming a scheme to a scheme reflecting a given property.}",
  affiliation   = "INRIA Bordeaux - Sud-Ouest - INRIA Bordeaux - Sud-Ouest , Laboratoire Bordelais de Recherche en Informatique - LaBRI",
  date-added    = "2013-03-27 13:35:18 +0000",
  date-modified = "2014-03-21 14:41:33 +0000",
  hal_id        = "hal-00741077",
  Language      = "Anglais",
  PDF           = "http://hal.inria.fr/hal-00741077/PDF/m.pdf",
  Title         = "{Using models to model-check recursive schemes}",
  URL           = "http://hal.inria.fr/hal-00741077",
  Year          = "2012",
  bdsk-url-1    = "http://hal.inria.fr/hal-00741077",
  File          = "Using models to model-check recursive schemes - Salvati, Walukiewicz (0) (1) - a - a - g.pdf",
  file-2        = "Using models to model-check recursive schemes - Salvati, Walukiewicz (0) (0) - a - a - g.graffle"
}

@TechReport{ salvati:hal-00741077, Author = "Salvati, Sylvain and Walukiewicz, Igor", Abstract = "{We propose a model-based approach to the model checking problem for recursive schemes. Since simply typed lambda calculus with the fixpoint operator, lambda-Y-calculus, is equivalent to schemes, we propose to use a model of lambda-Y to discriminate the terms that satisfy a given property. If a model is finite in every type, this gives a decision procedure. We provide a construction of such a model for every property expressed by automata with trivial acceptance conditions and divergence testing. We argue that having a model capable of recognizing terms satisfying a given property has other benefits than just providing decidability of the model-checking problem. We show a very simple construction transforming a scheme to a scheme reflecting a given property.}", affiliation = "INRIA Bordeaux - Sud-Ouest - INRIA Bordeaux - Sud-Ouest , Laboratoire Bordelais de Recherche en Informatique - LaBRI", date-added = "2013-03-27 13:35:18 +0000", date-modified = "2014-03-21 14:41:33 +0000", hal_id = "hal-00741077", Language = "Anglais", PDF = "http://hal.inria.fr/hal-00741077/PDF/m.pdf", Title = "{Using models to model-check recursive schemes}", URL = "http://hal.inria.fr/hal-00741077", Year = "2012", bdsk-url-1 = "http://hal.inria.fr/hal-00741077", File = "Using models to model-check recursive schemes - Salvati, Walukiewicz (0) (1) - a - a - g.pdf", file-2 = "Using models to model-check recursive schemes - Salvati, Walukiewicz (0) (0) - a - a - g.graffle" }