P. Amiranoff, A. Cohen, and P. Feautrier, Beyond Iteration Vectors: Instancewise Relational Abstract Domains, Static Analysis Symposium (SAS'06), 2006.
DOI : 10.1007/11823230_11
URL : https://hal.archives-ouvertes.fr/hal-01257289

]. W. Advf01, N. Amme, J. Dalton, M. Von-ronne, and . Franz, SafeTSA: a type safe and referentially secure mobile-code representation based on static single assignment form, ACM Symp. on Programming Language Design and Implementation (PLDI'01)

K. [. Allen and . Kennedy, Automatic translation of FORTRAN programs to vector form, ACM Transactions on Programming Languages and Systems, vol.9, issue.4, pp.491-542, 1987.
DOI : 10.1145/29873.29875

H. A¨?ta¨?t-kaci, Warren's Abstract Machine a Tutorial Reconstruction, 1999.

K. [. Allen and . Kennedy, Optimizing Compilers for Modern Architectures, 2002.

]. P. Ami04 and . Amiranoff, Analyse de programmes par instances par le biais des transducteurs, 2004.

M. [. Alpern, F. K. Wegman, and . Zadeck, Detecting equality of values in programs, POPL '88: Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp.1-11, 1988.

J. Backus, Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs, Communications of the ACM, vol.21, issue.8, pp.613-641, 1978.
DOI : 10.1145/359576.359579

[. Briggs, K. D. Cooper, T. J. Harvey, and L. T. Simpson, Practical improvements to the construction and destruction of static single assignment form. Software Practice and Experience, pp.859-881, 1998.

[. Berlin, D. Edelsohn, and S. Pop, High-level loop optimizations for GCC, Proceedings of the 2004 GCC Developers Summit, pp.37-54, 2004.

M. Marc, H. Brandis, and . Mossenbock, Single-pass generation of static single-assignment form for structured languages

[. Bilardi and K. Pingali, The static single assignment form and its computation, 1999.

[. Bilardi and K. Pingali, Algorithms for computing the static single assignment form, Journal of the ACM, vol.50, issue.3, pp.375-425, 2003.
DOI : 10.1145/765568.765573

[. Bachmann, P. S. Wang, and E. V. Zima, Chains of recurrences a method to expedite the evaluation of closedform functions, Proceedings of the international symposium on Symbolic and algebraic computation, pp.242-249, 1994.

R. [. Cousot and . 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/inria-00528590

R. [. Cousot and . Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '79, pp.269-282, 1979.
DOI : 10.1145/567752.567778

. Cfr-+-89-]-r, J. Cytron, B. K. Ferrante, M. N. Rosen, F. K. Wegman et al., An efficient method of computing static single assignment form, POPL '89: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.25-35, 1989.

. Cfr-+-91-]-r, J. Cytron, B. K. Ferrante, M. N. Rosen, F. K. Wegman et al., Efficiently computing static single assignment form and the control dependence graph, ACM Trans. on Programming Languages and Systems, vol.13, issue.4, pp.451-490, 1991.

N. [. Cousot and . Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '78, pp.84-96, 1978.
DOI : 10.1145/512760.512770

P. Clauss, Counting solutions to linear and nonlinear constraints through Ehrhart polynomials: Applications to analyze and transform scientific programs, ACM Int. Conf. on Supercomputing, pp.278-295, 1996.
URL : https://hal.archives-ouvertes.fr/hal-01100306

]. Cla96b, . Ph, and . Clauss, Counting solutions to linear and nonlinear constraints through ehrhart polynomials: Applications to analyze and transform scientific programs, ICS '96: Proceedings of the 10th international conference on Supercomputing, 1996.

. Ph, I. Clauss, and . Tchoupaeva, A symbolic approach to bernstein expansion for program analysis and optimization, 13th International Conference on Compiler Construction number 2985 in LNCS, 2004.

Y. [. Darte, F. Robert, and . Vivien, Scheduling and Automatic Parallelization, Birkhaser, 2000.
DOI : 10.1007/978-1-4612-1362-8
URL : https://hal.archives-ouvertes.fr/hal-00856645

[. Dvorak, Enable unrolling/peeling/unswitching of arbitrary loops

A. E. Eichenberger, P. Wu, and K. O. Brien, Vectorization for simd architectures with alignment constraints, PLDI '04: Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, pp.82-93, 2004.

J. Feret, Static Analysis of Digital Filters, European Symposium on Programming number 2986 in LNCS, 2004.
DOI : 10.1007/978-3-540-24725-8_4
URL : https://hal.archives-ouvertes.fr/inria-00528447

J. Feret, The Arithmetic-Geometric Progression Abstract Domain, Verification, Model Checking and Abstract Interpretation (VMCAI'05), number 3385 in LNCS, pp.42-58, 2005.
DOI : 10.1007/978-3-540-30579-8_3
URL : https://hal.archives-ouvertes.fr/inria-00528450

S. Glesner, An ASM Semantics for SSA Intermediate Representations, Proceedings of the 11th International Workshop on Abstract State Machines, 2004.
DOI : 10.1007/978-3-540-24773-9_11
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.68.405

J. C. Michael and . Gordon, The denotational description of programming languages, 1979.

P. Granger, Static analysis of linear congruence equalities among variables of a program, TAPSOFT '91: Proceedings of the international joint conference on theory and practice of software development on Colloquium on trees in algebra and programming (CAAP '91), pp.169-192, 1991.
DOI : 10.1007/3-540-53982-4_10

E. [. Gerlek, M. J. Stoltz, and . Wolfe, Beyond induction variables: detecting and classifying sequences using a demand-driven SSA form, ACM Transactions on Programming Languages and Systems, vol.17, issue.1, pp.85-122, 1995.
DOI : 10.1145/200994.201003
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.1476

Y. Gurevich, Evolving algebras 1993: Lipari guide, Specification and Validation Methods, pp.231-243, 1995.

P. Havlak, Construction of thinned gated single-assignment form, Proceedings of the 6th International Workshop on Languages and Compilers for Parallel Computing, pp.477-499, 1993.
DOI : 10.1007/3-540-57659-2_28

]. L. Hde-+-93, C. Hendren, M. Donawa, G. R. Emami, . Gao et al., Designing the McCAT compiler based on a family of structured intermediate representations, Proceedings of the 5th International Workshop on Languages and Compilers for Parallel Computing, number 757 in LNCS, pp.406-420, 1993.

]. C. Hoa69 and . Hoare, An axiomatic basis for computer programming, Commun. ACM, vol.12, issue.10, pp.576-580, 1969.

C. [. Haghighat and . Polychronopoulos, Symbolic analysis for parallelizing compilers, ACM Transactions on Programming Languages and Systems, vol.18, issue.4, pp.477-518, 1996.
DOI : 10.1145/233561.233568

N. D. Jones, Computability and Complexity from a Programming Perspective, 1997.
DOI : 10.1007/978-94-010-0413-8_4

A. Richard and . Kelsey, A correspondence between continuation passing style and static single assignment form, ACM SIGPLAN Notices, vol.30, issue.3, pp.13-22, 1995.

V. [. Kislenkov, E. Mitrofanov, and . Zima, Multidimensional chains of recurrences, Proceedings of the 1998 international symposium on Symbolic and algebraic computation , ISSAC '98, pp.199-206, 1998.
DOI : 10.1145/281508.281613

V. [. Lattner and . Adve, LLVM: A compilation framework for lifelong program analysis & transformation, International Symposium on Code Generation and Optimization, 2004. CGO 2004., 2004.
DOI : 10.1109/CGO.2004.1281665

K. [. Li and . Pingali, A singular loop transformation framework based on non-singular matrices, International Journal of Parallel Programming, vol.16, issue.4, pp.183-205, 1994.
DOI : 10.1007/BF02577874
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.9703

D. Luna, M. Pettersson, and K. Sagonas, Efficiently compiling a functional language on AMD64, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming , PPDP '05, pp.176-186, 2005.
DOI : 10.1145/1069774.1069791

D. [. Loechner and . Wilde, Parameterized polyhedra and their vertices, Int. J. of Parallel Programming, vol.25, issue.6, 1997.
URL : https://hal.archives-ouvertes.fr/inria-00534851

[. Masdupuy, Array abstractions using semantic analysis of trapezoid congruences, Proceedings of the 6th international conference on Supercomputing , ICS '92, pp.226-235, 1992.
DOI : 10.1145/143369.143414

]. F. Mas93 and . Masdupuy, Semantic analysis of interval congruences, Intl. Conf. on Formal Methods in Programming and their Applications, pp.142-155, 1993.

J. Merill, GENERIC and GIMPLE: a new tree representation for entire functions, Proceedings of the 2003 GCC Developers Summit, pp.171-180, 2003.

A. Miné, The octagon abstract domain, IEEE, pp.310-319, 2001.

]. R. Moo66 and . Moore, Interval Analysis, Englewood Cliffs N. J, 1966.

]. S. Muc97 and . Muchnick, Advanced Compiler Design & Implementation, 1997.

D. Naishlos, Autovectorization in GCC, Proceedings of the 2004 GCC Developers Summit, pp.105-118, 2004.

D. Nuzman and R. Henderson, Multi-platform autovectorization, Proceedings 4th Annual International Symposium on Code Generation and Optimization, 2006.

H. [. Nielson, C. Nielson, and . Hankin, Principles of Program Analysis, 1999.
DOI : 10.1007/978-3-662-03811-6

D. Novillo, SIMPLE: A language-independent tree IR

D. Novillo, Tree SSA -a new optimization infrastructure for GCC, Proceedings of the 2003 GCC Developers Summit, pp.181-193, 2003.

D. Novillo, A propagation engine for GCC, Proceedings of the 2005 GCC Developers Summit, pp.175-185, 2005.

D. Nuzman, I. Rosen, and A. Zaks, Auto-vectorization of interleaved data for SIMD, Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI, 2006.

D. Nuzman and A. Zaks, Autovectorization in GCC ? two years later, Proceedings of the 2006 GCC Developers Summit, pp.145-158, 2006.

S. Nikolaos and . Papaspyrou, A Formal Semantics for the C Programming Language, 1998.

R. C. Jason and . Patterson, Accurate static branch prediction by value range propagation, SIGPLAN Conference on Programming Language Design and Implementation, pp.67-78, 1995.

A. Sebastian-pop, C. Cohen, S. Bastoul, G. Girbal, N. Silber et al., Graphite: Polyhedral analyses and optimizations for GCC, Proc. of the 4 th GCC Developper's Summit, 2006.

S. Pop, P. Clauss, A. Cohen, V. Loechner, and G. Silber, Fast recognition of scalar evolutions on three-address SSA code, Centre de Recherche en Informatique (CRI), ´ Ecole des mines de Paris, 2004.

[. Pop, A. Cohen, P. Jouvelot, and G. Silber, Denotational semantics for SSA conversion, Centre de Recherche en Informatique (CRI), ´ Ecole des mines de Paris, 2006.

[. Pop, A. Cohen, P. Jouvelot, and G. Silber, The new framework for loop nest optimization in GCC: from prototyping to evaluation, Proc. of the 12 th Workshop on Compilers for Parallel Computers (CPC'06), 2006.
URL : https://hal.archives-ouvertes.fr/hal-01257285

[. Pop, A. Cohen, and G. Silber, Induction Variable Analysis with Delayed Abstractions, (HiPEAC'05), number 3793 in LNCS, pp.218-232, 2005.
DOI : 10.1007/11587514_15
URL : https://hal.archives-ouvertes.fr/hal-01257294

]. W. Pug92 and . Pugh, A practical algorithm for exact array dependence analysis, Communications of the ACM, vol.35, issue.8, pp.27-47, 1992.

M. [. Paterson and . Wegman, Linear unification, STOC '76: Proceedings of the eighth annual ACM symposium on Theory of computing, pp.181-186, 1976.

M. [. Paterson and . Wegman, Linear unification, Journal of Computer and System Sciences, vol.16, issue.2, pp.158-167, 1978.
DOI : 10.1016/0022-0000(78)90043-0

H. Rogers, Theory of Recursive Functions and Effective Computability, 1987.

M. [. Rosen, F. K. Wegman, and . Zadeck, Global value numbers and redundant computations, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '88, pp.12-27, 1988.
DOI : 10.1145/73560.73562

[. Rus, D. Zhang, and L. Rauchwerger, The value evolution graph and its use in memory reference analysis, Proceedings. 13th International Conference on Parallel Architecture and Compilation Techniques, 2004. PACT 2004., 2004.
DOI : 10.1109/PACT.2004.1342558

D. S. Scott, Domains for denotational semantics, Proceedings of the 9th Colloquium on Automata, Languages and Programming, pp.577-613, 1982.
DOI : 10.1007/BFb0012801

C. Vugranam, R. Sreedhar, D. M. Dz-ching-ju, V. Gillies, and . Santhanam, Translating out of static single assignment form, SAS '99: Proceedings of the 6th International Symposium on Static Analysis, pp.194-210, 1999.

C. Strachey and R. Milne, A theory of programming language semantics, 1976.

H. [. Shapiro and . Saint, The representation of algorithms, 1970.

E. Joseph and . Stoy, Denotational Semantics: the Scott-Strachey Approach to Programming Languages Theory, 1977.

]. R. Tar74 and . Tarjan, Finding dominators in directed graphs, SIAM J. Computing, vol.3, issue.1, pp.62-89, 1974.

]. P. Tp95a, D. Tu, and . Padua, Gated SSA-Based demand-driven symbolic analysis for parallelizing compilers, ACM Int. Conf. on Supercomputing, pp.414-423, 1995.

P. Tu and D. Padua, Efficient building and placing of gating functions, Proceedings of the ACM SIGPLAN 1995 Conference on Programming Language Design and Implementation, pp.47-55, 1995.

R. A. Van-engelen, Efficient Symbolic Analysis for Optimizing Compilers, Proceedings of the International Conference on Compiler Construction (ETAPS CC'01), pp.118-132, 2001.
DOI : 10.1007/3-540-45306-7_9

R. Van-engelen, J. Birch, Y. Shou, B. Walsh, and K. Gallivan, A unified framework for nonlinear dependence testing and symbolic analysis, Proceedings of the 18th annual international conference on Supercomputing , ICS '04, pp.106-115, 2004.
DOI : 10.1145/1006209.1006226

A. Venet, Nonuniform Alias Analysis of Recursive Data Structures and Arrays, Proceedings of the 9th International Symposium on Static Analysis SAS'02, number 2477 in LNCS, pp.36-51, 2002.
DOI : 10.1007/3-540-45789-5_6

A. [. Wu, D. Cohen, and . Padua, Induction Variable Analysis without Idiom Recognition: Beyond Monotonicity, Workshop on Languages and Compilers for Parallel Computing, 2001.
DOI : 10.1007/3-540-35767-X_28
URL : https://hal.archives-ouvertes.fr/hal-01257311

]. M. Wol92 and . Wolfe, Beyond induction variables, ACM Symp. on Programming Language Design and Implementation (PLDI'92), pp.162-174, 1992.

]. M. Wol96 and . Wolfe, High Performance Compilers for Parallel Computing, 1996.

F. [. Wegman and . Zadeck, Constant propagation with conditional branches, ACM Transactions on Programming Languages and Systems, vol.13, issue.2, pp.181-210, 1991.
DOI : 10.1145/103135.103136

]. F. Zada and . Zadeck, Loop closed SSA form

]. F. Zadb and . Zadeck, Static single assignment form, GCC Summit keynote, 2004.

E. V. Zima, On computational properties of chains of recurrences, Proceedings of the 2001 international symposium on Symbolic and algebraic computation , ISSAC '01, pp.345-352, 2001.
DOI : 10.1145/384101.384148