D. Armando, Y. Basin, Y. Boichut, L. Chevalier, J. Compagna et al., The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications, CAV'2005, pp.281-285, 2005.
DOI : 10.1007/11513988_27
URL : https://hal.archives-ouvertes.fr/inria-00000408

B. [. Boichut, T. Boyer, A. Genet, and . Legay, Equational Abstraction Refinement for Certified Tree Regular Model Checking, ICFEM'12, 2012.
DOI : 10.1007/978-3-642-34281-3_22
URL : https://hal.archives-ouvertes.fr/hal-00759149

P. [. Bertot and . Castéran, Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

R. [. Boichut, P. Courbis, O. Héam, and . Kouchnarenko, Handling non leftlinear rules when completing tree automata, IJFCS, vol.20, issue.5, 2009.
URL : https://hal.archives-ouvertes.fr/hal-00561373

T. [. Boyer, T. Genet, and . Jensen, Certifying a Tree Automata Completion Checker, IJCAR'08, 2008.
DOI : 10.1007/978-3-540-71070-7_43
URL : https://hal.archives-ouvertes.fr/inria-00258275

T. [. Boichut, T. Genet, L. Jensen, and . Leroux, Rewriting Approximations for Fast Prototyping of Static Analyzers, RTA, pp.48-62, 2007.
DOI : 10.1007/978-3-540-73449-9_6
URL : https://hal.archives-ouvertes.fr/hal-00463418

F. Baader and T. Nipkow, Term Rewriting and All That, 1998.

H. Comon and J. Rémy, How to characterize the language of ground normal forms, 1987.
URL : https://hal.archives-ouvertes.fr/inria-00075877

G. Feuillade, T. Genet, V. Viet-triem, and . Tong, Reachability Analysis over Term Rewriting Systems, Journal of Automated Reasoning, vol.37, issue.1?2, pp.3-4341, 2004.
DOI : 10.1007/s10817-004-6246-0
URL : https://hal.archives-ouvertes.fr/inria-00071609

T. Genet, Decidable approximations of sets of descendants and sets of normal forms, Proc. 9th RTA Conf., Tsukuba (Japan), volume 1379 of LNCS, pp.151-165, 1998.
DOI : 10.1007/BFb0052368
URL : https://hal.archives-ouvertes.fr/inria-00073364

D. [. Geser, J. Hofbauer, H. Waldmann, and . Zantema, On tree automata that certify termination of left-linear term rewriting systems, RTA'05, pp.353-367, 2005.

F. [. Genet and . Klay, Rewriting for Cryptographic Protocol Verification, Proc. 17th CADE Conf., Pittsburgh (Pen., USA), volume 1831 of LNAI, 2000.
DOI : 10.1007/10721959_21
URL : https://hal.archives-ouvertes.fr/inria-00072731

T. Genet and R. Rusu, Equational approximations for tree automata completion, Journal of Symbolic Computation, vol.45, issue.5, pp.574-597, 2010.
DOI : 10.1016/j.jsc.2010.01.009
URL : https://hal.archives-ouvertes.fr/inria-00495405

R. [. Giesl, P. Thiemann, S. Schneider-kamp, and . Falke, Mechanizing and Improving Dependency Pairs, Journal of Automated Reasoning, vol.34, issue.2, pp.155-203, 2006.
DOI : 10.1007/s10817-006-9057-7

]. N. Jon87 and . Jones, Flow analysis of lazy higher-order functional programs, Abstract Interpretation of Declarative Languages, pp.103-122, 1987.

J. Kochems and L. Ong, Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars, RTA'11 of LIPIcs. Schloss Dagstuhl?Leibniz-Zentrum fuer Informatik, 2011.

]. X. Ldg-+-12, D. Leroy, J. Doligez, D. Garrigue, J. Rémy et al., The Objective Caml system release 3.12 ? Documentation and user's manual. INRIA, 2012.

]. A. Lis12 and . Lisitsa, Finite Models vs Tree Automata in Safety Verification, RTA'12, pp.225-239, 2012.

]. A. Mid02 and . Middeldorp, Approximations for strategies and termination, ENTCS, vol.70, issue.6, pp.1-20, 2002.

S. [. Ong and . Ramsay, Verifying higher-order functional programs with patternmatching algebraic data types, POPL'11, 2011.

P. Réty and J. Vuotto, Regular Sets of Descendants by Some Rewrite Strategies, Proc. 13th RTA Conf, 2002.
DOI : 10.1007/3-540-45610-4_10

T. Takai, Y. Kaji, and H. Seki, Right-Linear Finite Path Overlapping Term Rewriting Systems Effectively Preserve Recognizability, Proc. 11th RTA Conf., Norwich (UK), volume 1833 of LNCS, 2000.
DOI : 10.1007/10721975_17