Document Open Access Logo

Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars

Authors Jonathan Kochems, C.H. Luke Ong



PDF
Thumbnail PDF

File

LIPIcs.RTA.2011.187.pdf
  • Filesize: 0.57 MB
  • 16 pages

Document Identifiers

Author Details

Jonathan Kochems
C.H. Luke Ong

Cite AsGet BibTex

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)
https://doi.org/10.4230/LIPIcs.RTA.2011.187

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.
Keywords
  • Flow analysis
  • reachability
  • collecting semantics
  • higher-order program
  • term rewriting
  • indexed linear tree grammar

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail