. Soit-f:-u-?-?-?-u-un-opérateur and . Concret, On souhaite construire un opérateur abstrait ? : U ? ? ? ? U ? tel que pour toute approximation correcte x de P , ?(x) soit une approximation correcte de f (P )

[. Boichut and P. Héam, A theoretical limit for safety verification techniques with regular fix-point computations, Information Processing Letters, vol.108, issue.1, pp.1-2, 2008.
DOI : 10.1016/j.ipl.2008.03.012
URL : https://hal.archives-ouvertes.fr/inria-00328487

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

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

B. Boyer, Réécriture d'automates certifiée pour la vérification de modèles, Thèse de doctorat, 2010.

[. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/hal-01108790

[. Cousot and R. Cousot, Formal language, grammar and set-constraint-based program analysis by abstract interpretation, Proceedings of the seventh international conference on Functional programming languages and computer architecture , FPCA '95, 1995.
DOI : 10.1145/224164.224199

[. Comon and F. Jacquemard, « Ground reducibility is EXPTIMEcomplete, Inf. Comput, vol.1871, pp.123-153, 2003.

H. Cirstea, S. Lenglet, and P. Moreau, « A faithful encoding of programmable strategies into term rewriting systems Sous la dir. de Maribel Fernández. T. 36, 26th International Conference on Rewriting Techniques and Applications Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany : Schloss Dagstuhl?Leibniz-Zentrum fuer Informatik, pp.74-88, 2015.

H. Comon, Complexité du calcul de l'automate des formes normales. Communication privée, 2013.

C. Bibliographie and . Coquidé, Bottom-up tree pushdown automata and rewrite systems Rewriting Techniques and Applications. Sous la dir. de Ronald Book. T. 488, Lecture Notes in Computer Science, vol.10, pp.287-2983, 1991.

[. Cousot, Analyseur statique de logiciels temps-réel embarqués (ASTRÉE)

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-4, 2004.
DOI : 10.1007/s10817-004-6246-0
URL : https://hal.archives-ouvertes.fr/inria-00071609

M. Frigo, G. Steven, and . Johnson, The Fastest Fourier Transform in the West, 2015.

H. Jean, R. V. Gallier, and . Book, « Reductions in Tree Replacement Systems, Theor. Comput. Sci, vol.37, pp.123-150, 1985.

[. Genet, Timbuk 3 ? A Tree Automata Completion Tool, IRISA / Université de Rennes, vol.1, 2008.

T. Genet, « Reachability analysis of rewriting for Software verification ». Thèse d'habilitation à diriger des recherches, 2009.

T. Genet, A Note on the Precision of the Tree Automata Completion
URL : https://hal.archives-ouvertes.fr/hal-01091393

T. Genet, Termination criteria for tree automata completion, Journal of Logical and Algebraic Methods in Programming, vol.85, issue.1, pp.2352-2208, 2015.
DOI : 10.1016/j.jlamp.2015.05.003
URL : https://hal.archives-ouvertes.fr/hal-01194533

[. 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, 1997.
DOI : 10.1007/BFb0052368
URL : https://hal.archives-ouvertes.fr/inria-00073364

[. Gascon, G. Godoy, and F. Jacquemard, Closure of Tree Automata Languages under Innermost Rewriting ». Anglais In : 8th International Workshop on Reduction Strategies in Rewriting and Programming (WRS). T. 237, ENTCS. Hagenberg, pp.23-38, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00578966

[. Genet and F. Klay, Rewriting for Cryptographic Protocol Verification (extended version), 2000.
URL : https://hal.archives-ouvertes.fr/inria-00072731

[. Genet, B. Kordy, and A. Vansyngel, « Vers un outil de vérification formelle légere pour OCaml

P. John, G. Gallagher, and . Puebla, « Abstract Interpretation over Non-Deterministic Finite Tree Automata for Set-Based Analysis of Logic Programs, Fourth International Symposium on Practical Aspects of Declarative Languages, number 2257 in LNCS, pp.243-261, 2002.

[. Genet and V. 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

[. Genet and Y. Salmon, « Reachability Analysis of Innermost Rewriting Sous la dir. de Maribel Fernández. T. 36. Leibniz International Proceedings in Informatics (LIPIcs) Dagstuhl, Germany : Schloss Dagstuhl?Leibniz-Zentrum fuer Informatik, 26th International Conference on Rewriting Techniques and Applications, pp.177-193, 2015.

[. Gilleron and S. Tison, « Regular Tree Languages and Rewrite Systems, pp.157-175, 1995.

[. Genet, V. Viet-triem, and . Tong, Timbuk ? A Tree Automata Library. IRISA / Université de Rennes 1, 2001.

D. Neil, S. Jones-et-steven, and . Muchnick, « Flow Analysis and Optimization of LISP-like structures, pp.244-256, 1979.

J. Simon-peyton, The Haskell Programming Language, 1990.

J. Jouannaud, Sous la dir. d'Aart Middeldorp et al. T. 3838. Lecture Notes in Computer Science, Higher-Order Rewriting : Framework, Confluence and Termination ». English. In : Processes, Terms and Cycles : Steps on the Road to Infinity, 2005.

[. Jouannaud, F. Van-rammsdonk, and A. Rubio, Higherorder Rewriting with Types and Arities

X. Leroy, The Objective Caml system. INRIA. http://caml.inria.fr/ocaml, 1996.

V. Murat, Tree automata extensions for verification of infinite states systems, Theses. Université Rennes, vol.1
URL : https://hal.archives-ouvertes.fr/tel-01065696

[. Ong and S. J. Ramsay, « Verifying Higher-Order Functional Programs with Pattern Matching Algebraic Data Types, Proceedings of the 38th ACM SIGACT-SIGPLAN Symposium on the Principles of Programming Languages (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, Regular Sets of Descendants for Constructor-Based Rewrite Systems Sous la dir. d'Harald Ganzinger, David McAllester et Andrei Voronkov . T. 1705. Lecture Notes in Computer Science. 10.1007/3-540- 48242-3_10, Logic for Programming and Automated Reasoning, pp.148-160, 1999.

R. Henry-gordon, Classes of Recursively Enumerable Sets and Their Decision Problems, Transactions of the American Mathematical Society, vol.742, pp.358-366, 1953.

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

K. «. Salomaa, Deterministic tree pushdown automata and monadic tree rewriting systems, Journal of Computer and System Sciences, vol.37, issue.3, pp.367-3940022, 1988.
DOI : 10.1016/0022-0000(88)90014-1

A. David and . Schmidt, Denotational semantics : a methodology for language development, p.205089747, 1986.

T. Takai, A Verification Technique Using Term Rewriting Systems and Abstract Interpretation, Rapport. Japan Science et Technology Corporation, 2004.
DOI : 10.1007/978-3-540-25979-4_9

A. Mathison and T. , « On Computable Numbers, with an Application to the Entscheidungsproblem, Proceedings of the London Mathematical Society. Second Series, vol.42, pp.230-265, 1936.

G. Winskel, The formal semantics of programming languages : an introduction . Foundations of computing, Cambridge (Mass.), p.262231697, 1993.