DROPS

Document

DOI: 10.4230/LIPIcs.RTA.2011.187

Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars

Authors: Jonathan Kochems and C.H. Luke Ong

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

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.

Cite as

Jonathan Kochems and C.H. Luke Ong. Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 187-202, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{kochems_et_al:LIPIcs.RTA.2011.187,
  author =	{Kochems, Jonathan and Ong, C.H. Luke},
  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 =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.187},
  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}
}

Search Results

Documents authored by Kochems, Jonathan

Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars

Abstract

Cite as

Thanks for your feedback!

Could not send message