Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Haddad, Axel http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-43605
URL:

Model Checking and Functional Program Transformations

pdf-format:


Abstract

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 pushdown automata and they lose 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.

BibTeX - Entry

@InProceedings{haddad:LIPIcs:2013:4360,
  author =	{Axel Haddad},
  title =	{{Model Checking and Functional Program Transformations}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)},
  pages =	{115--126},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-64-4},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{24},
  editor =	{Anil Seth and Nisheeth K. Vishnoi},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4360},
  URN =		{urn:nbn:de:0030-drops-43605},
  doi =		{10.4230/LIPIcs.FSTTCS.2013.115},
  annote =	{Keywords: Higher-order recursion schemes, Model checking, Tree automata}
}

Keywords: Higher-order recursion schemes, Model checking, Tree automata
Seminar: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)
Issue date: 2013
Date of publication: 2013


DROPS-Home | Fulltext Search | Imprint Published by LZI