License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2015.177
URN: urn:nbn:de:0030-drops-51968
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5196/
Go to the corresponding LIPIcs Volume Portal

Genet, Thomas ; Salmon, Yann

Reachability Analysis of Innermost Rewriting

pdf-format:
16.pdf (0.6 MB)

Abstract

We consider the problem of inferring a grammar describing the output of a functional program given a grammar describing its input. Solutions to this problem are helpful for detecting bugs or proving safety properties of functional programs and, several rewriting tools exist for solving this problem. However, known grammar inference techniques are not able to take evaluation strategies of the program into account. This yields very imprecise results when the evaluation strategy matters. In this work, we adapt the Tree Automata Completion algorithm to approximate accurately the set of
terms reachable by rewriting under the innermost strategy. We prove that the proposed technique is sound and precise w.r.t. innermost rewriting. The proposed algorithm has been implemented in the Timbuk reachability tool. Experiments show that it noticeably improves the accuracy of static analysis for functional programs using the call-by-value evaluation strategy.

BibTeX - Entry

@InProceedings{genet_et_al:LIPIcs:2015:5196,
  author =	{Thomas Genet and Yann Salmon},
  title =	{{Reachability Analysis of Innermost Rewriting}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{177--193},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Maribel Fern{\'a}ndez},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5196},
  URN =		{urn:nbn:de:0030-drops-51968},
  doi =		{10.4230/LIPIcs.RTA.2015.177},
  annote =	{Keywords: term rewriting systems, strategy, innermost strategy, tree automata, functiona l program, static analysis}
}

Keywords: term rewriting systems, strategy, innermost strategy, tree automata, functiona l program, static analysis
Collection: 26th International Conference on Rewriting Techniques and Applications (RTA 2015)
Issue Date: 2015
Date of publication: 18.06.2015

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