文章基本信息

标题：Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars
本地全文：下载
作者：Jonathan Kochems ; C.H. Luke Ong
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2011
卷号：10
页码：187-202
DOI：10.4230/LIPIcs.RTA.2011.187
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Flow analysis; reachability; collecting semantics; higher-order program; term rewriting; indexed linear tree grammar