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

. Aprove, Automated Program Verification Environment

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. [. 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

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

O. Danvy and A. Filinski, Representing Control: a Study of the CPS Transformation, Mathematical Structures in Computer Science, vol.598, issue.04, pp.361-391, 1992.
DOI : 10.1016/0304-3975(87)90109-5

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

A. Gascon, G. Godoy, and F. Jacquemard, Closure of Tree Automata Languages under Innermost Rewriting, 8th International Workshop on Reduction Strategies in Rewriting and Programming (WRS), pp.23-38, 2008.
DOI : 10.1016/j.entcs.2009.03.033

URL : https://hal.archives-ouvertes.fr/inria-00578966

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

Y. [. Genet and . Salmon, Tree Automata Completion for Static Analysis of Functional Programs
URL : https://hal.archives-ouvertes.fr/hal-00780124

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.

N. Kobayashi and A. Igarashi, Model-Checking Higher-Order Programs with Recursive Types, ESOP, pp.431-450, 2013.
DOI : 10.1007/978-3-642-37036-6_24

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.

]. 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.

G. D. Plotkin, Call-by-name, call-by-value and the ??-calculus, Theoretical Computer Science, vol.1, issue.2, pp.125-159, 1975.
DOI : 10.1016/0304-3975(75)90017-1

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