DI-UMONS : Dépôt institutionnel de l’université de Mons

Recherche transversale
Rechercher
(titres de publication, de périodique et noms de colloque inclus)
2013-12-14 - Colloque/Article dans les actes avec comité de lecture - Anglais - 12 page(s)

Haddad Axel , "Model Checking and Functional Program Transformations" in IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS, 115-126, Guwahati, Inde, 2013

  • Codes CREF : Informatique mathématique (DI1160)
  • Unités de recherche UMONS : Mathématiques effectives (S820)
  • Instituts UMONS : Institut de Recherche sur les Systèmes Complexes (Complexys)
  • Centres UMONS : Modélisation mathématique et informatique (CREMMI)

Abstract(s) :

(Anglais) We study a model for recursive functional programs called, higher order recursion schemes (HORS). We give new proofs of two verification related problems: reflection and selection for HORS. The previous proofs are based on the equivalence between HORS and collapsible push-down automata and they looses the structure of the initial program. The constructions presented here are based on shape preserving transformations, and can be applied on actual programs without losing the structure of the program.

Identifiants :
  • DOI : 10.1109/LICS.2011.28

Mots-clés :
  • (Anglais) Model-checking
  • (Anglais) higher-order recursion schemes
  • (Anglais) Program transformation
  • (Anglais) Tree grammars