Document Open Access Logo

Reachability Analysis of Innermost Rewriting

Authors Thomas Genet, Yann Salmon

PDF
Thumbnail PDF

File

LIPIcs.RTA.2015.177.pdf
  • Filesize: 0.59 MB
  • 17 pages

Document Identifiers

Author Details

Thomas Genet
Yann Salmon

Cite As Get BibTex

Thomas Genet and Yann Salmon. Reachability Analysis of Innermost Rewriting. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 177-193, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.RTA.2015.177

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.

Subject Classification

Keywords
  • term rewriting systems
  • strategy
  • innermost strategy
  • tree automata
  • functiona l program
  • static analysis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  2. Y. Boichut, J. Chabin, and P. Réty. Over-approximating descendants by synchronized tree languages. In RTA'13, volume 21 of LIPIcs, pages 128-142. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013. Google Scholar
  3. Y. Boichut, R. Courbis, P.-C. Héam, and O. Kouchnarenko. Handling non left-linear rules when completing tree automata. IJFCS, 20(5), 2009. Google Scholar
  4. C. H. Broadbent, A. Carayol, M. Hague, and O. Serre. C-shore: a collapsible approach to higher-order verification. In ICFP'13. ACM, 2013. Google Scholar
  5. G. Castagna, K. Nguyen, Z. Xu, H. Im, S. Lenglet, and L. Padovani. Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation. In POPL'14. ACM, 2014. Google Scholar
  6. H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, C. Löding, S. Tison, and M. Tommasi. Tree automata techniques and applications. http://tata.gforge.inria.fr, 2008. Google Scholar
  7. H. Comon and Jean-Luc Rémy. How to characterize the language of ground normal forms. Technical Report 676, INRIA-Lorraine, 1987. Google Scholar
  8. G. Feuillade, T. Genet, and V. Viet Triem Tong. Reachability Analysis over Term Rewriting Systems. Journal of Automated Reasonning, 33 (3-4):341-383, 2004. Google Scholar
  9. A. Gascon, G. Godoy, and F. Jacquemard. Closure of Tree Automata Languages under Innermost Rewriting. In WRS'08, volume 237 of ENTCS, pages 23-38. Elsevier, 2008. Google Scholar
  10. T. Genet. Decidable Approximations of Sets of Descendants and Sets of Normal Forms. In RTA'98, volume 1379 of LNCS, pages 151-165. Springer, 1998. Google Scholar
  11. T. Genet. A note on the Precision of the Tree Automata Completion. Technical report, INRIA, 2014. URL: https://hal.inria.fr/hal-01091393.
  12. T. Genet. Towards Static Analysis of Functional Programs using Tree Automata Completion. In WRLA'14, volume 8663 of LNCS. Springer, 2014. Google Scholar
  13. T. Genet, Y. Boichut, B. Boyer, V. Murat, and Y. Salmon. Reachability Analysis and Tree Automata Calculations. IRISA / Université de Rennes 1. URL: http://www.irisa.fr/celtique/genet/timbuk/.
  14. T. Genet and R. Rusu. Equational tree automata completion. Journal of Symbolic Computation, 45:574-597, 2010. Google Scholar
  15. T. Genet and Y. Salmon. Reachability Analysis of Innermost Rewriting. Technical report, INRIA, 2013. URL: http://hal.archives-ouvertes.fr/hal-00848260/PDF/main.pdf.
  16. T. Genet and Y. Salmon. Tree Automata Completion for Static Analysis of Functional Programs. Technical report, INRIA, 2013. URL: http://hal.archives-ouvertes.fr/hal-00780124/PDF/main.pdf.
  17. A. Geser, D. Hofbauer, J. Waldmann, and H. Zantema. On tree automata that certify termination of left-linear term rewriting systems. In RTA'05, volume 3467 of LNCS, pages 353-367. Springer, 2005. Google Scholar
  18. J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann. Proving termination of programs automatically with aprove. In IJCAR'14, volume 8562 of LNCS, pages 184-191. Springer, 2014. Google Scholar
  19. J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke. Mechanizing and improving dependency pairs. Journal of Automated Reasonning, 37(3):155-203, 2006. Google Scholar
  20. N. D. Jones and N. Andersen. Flow analysis of lazy higher-order functional programs. Theoretical Computer Science, 375(1-3):120-136, 2007. Google Scholar
  21. N. Kobayashi. Model Checking Higher-Order Programs. Journal of the ACM, 60.3(20), 2013. Google Scholar
  22. J. Kochems and L. Ong. Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars. In RTA'11, volume 10 of LIPIcs. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2011. Google Scholar
  23. A. Lisitsa. Finite Models vs Tree Automata in Safety Verification. In RTA'12, volume 15 of LIPIcs, pages 225-239, 2012. Google Scholar
  24. A. Middeldorp. Approximations for strategies and termination. ENTCS, 70(6):1-20, 2002. Google Scholar
  25. L. Ong and S. Ramsay. Verifying higher-order functional programs with pattern-matching algebraic data types. In POPL'11. ACM, 2011. Google Scholar
  26. P. Réty and J. Vuotto. Regular Sets of Descendants by some Rewrite Strategies. In RTA'02, volume 2378 of LNCS. Springer, 2002. Google Scholar
  27. T. Takai, Y. Kaji, and H. Seki. Right-linear finite-path overlapping term rewriting systems effectively preserve recognizability. In RTA'11, volume 1833 of LNCS. Springer, 2000. Google Scholar
  28. Terese. Term Rewriting Systems. Cambridge University Press, 2003. Google Scholar
  29. N. Vazou, P. Rondon, and R. Jhala. Abstract Refinement Types. In ESOP'13, volume 7792 of LNCS. Springer, 2013. Google Scholar
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact