License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2011.187
URN: urn:nbn:de:0030-drops-31167
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2011/3116/
Go to the corresponding LIPIcs Volume Portal

Kochems, Jonathan ; Ong, C.H. Luke

Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars

pdf-format:
9.pdf (0.6 MB)

Abstract

The collecting semantics of a program defines the strongest static property of interest. We study the analysis of the collecting semantics of higher-order functional programs, cast as left-linear term rewriting systems. The analysis generalises functional flow analysis and the reachability problem for term rewriting systems, which are both undecidable. We present an algorithm that uses indexed linear tree grammars (ILTGs) both to describe the input set and compute the set that approximates the collecting semantics. ILTGs are equi-expressive with pushdown tree automata, and so, strictly more expressive than regular tree grammars. Our result can be seen as a refinement of Jones and Andersen's procedure, which uses regular tree grammars. The main technical innovation of our algorithm is the use of indices to capture (sets of) substitutions, thus enabling a more precise binding analysis than afforded by regular grammars. We give a simple proof of termination and soundness, and demonstrate that our method is more accurate than other approaches to functional flow and reachability analyses in the literature.

BibTeX - Entry

@InProceedings{kochems_et_al:LIPIcs:2011:3116,
  author =	{Jonathan Kochems and C.H. Luke Ong},
  title =	{{Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{187--202},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9 },
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Manfred Schmidt-Schau{\ss}},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3116},
  URN =		{urn:nbn:de:0030-drops-31167},
  doi =		{10.4230/LIPIcs.RTA.2011.187},
  annote =	{Keywords: Flow analysis, reachability, collecting semantics, higher-order program, term rewriting, indexed linear tree grammar}
}

Keywords: Flow analysis, reachability, collecting semantics, higher-order program, term rewriting, indexed linear tree grammar
Collection: 22nd International Conference on Rewriting Techniques and Applications (RTA'11)
Issue Date: 2011
Date of publication: 26.04.2011

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI