LIPIcs.FSTTCS.2013.115.pdf
- Filesize: 0.49 MB
- 12 pages
Document
Model Checking and Functional Program Transformations
Author
-
Part of:
Volume:
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2013-12-10
Cite AsGet BibTex
Axel Haddad. Model Checking and Functional Program Transformations. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 115-126, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
https://doi.org/10.4230/LIPIcs.FSTTCS.2013.115
https://doi.org/10.4230/LIPIcs.FSTTCS.2013.115
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.
Keywords
- Higher-order recursion schemes
- Model checking
- Tree automata
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads