C. Alias, Program Optimization by Template Recognition and Replacement, 2005.

B. Godlin and O. Strichman, Regression verification: proving the equivalence of similar???programs, Software Testing, Verification and Reliability, vol.1738, issue.188, 2012.
DOI : 10.1002/stvr.1472

X. Feng and A. J. Hu, Cutpoints for formal equivalence verification of embedded software, Proceedings of the 5th ACM international conference on Embedded software , EMSOFT '05, 2005.
DOI : 10.1145/1086228.1086284

T. Hoare, The verifying compiler: A grand challenge for computing research, Journal of the ACM, vol.50, issue.1, pp.63-69, 2003.
DOI : 10.1145/602382.602403

G. C. Necula, Translation validation for an optimizing compiler, In: PLDI, pp.83-95, 2000.

A. Pnueli, M. Siegel, and F. Singerman, Translation validation, pp.151-166, 1998.
DOI : 10.1007/BFb0054170

L. Zuck, A. Pnueli, B. Goldberg, C. Barrett, Y. Fang et al., Translation and Run-Time Validation of Loop Transformations, Formal Methods in System Design, vol.9, issue.3, pp.335-360, 2005.
DOI : 10.1007/s10703-005-3402-z

S. Kundu, Z. Tatlock, and S. Lerner, Proving optimizations correct using parameterized program equivalence, 2009.
DOI : 10.1145/1543135.1542513
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.348.3828

D. Sangiorgi, Bisimulation and coinduction, Cambridge, 2012.
DOI : 10.1017/cbo9780511792588.002
URL : https://hal.archives-ouvertes.fr/hal-00907029

P. Jan?ar, Decidability of Bisimilarity for One-Counter Processes, Information and Computation, vol.158, issue.1, pp.1-17, 2000.
DOI : 10.1006/inco.1999.2813

D. Barthou, P. Feautrier, and X. Redon, On the equivalence of two systems of affine recurrence equations (research note), Proceedings of the 8th International Euro-Par Conference on Parallel Processing. Euro-Par '02, pp.309-313, 2002.

K. C. Shashidhar, M. Bruynooghe, F. Catthoor, and G. Janssens, Verification of Source Code Transformations by Program Equivalence Checking, Proceedings of the 14th International Conference on Compiler Construction. CC'05, pp.221-236, 2005.
DOI : 10.1007/978-3-540-31985-6_15

S. Verdoolaege, G. Janssens, and M. Bruynooghe, Equivalence checking of static affine programs using widening to handle recurrences, ACM Transactions on Programming Languages and Systems, vol.34, issue.3, pp.1-1135, 2012.
DOI : 10.1145/2362389.2362390

C. Karfa, K. Banerjee, D. Sarkar, and C. Mandal, Verification of loop and arithmetic transformations of array-intensive behaviors. Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on, vol.32, issue.11, pp.1787-1800, 2013.

D. B. West, Introduction to Graph Theory Introduction to Graph Theory, 1999.

P. Feautrier, Dataflow analysis of array and scalar references, International Journal of Parallel Programming, vol.24, issue.4, 1991.
DOI : 10.1007/BF01407931

X. Redon and P. Feautrier, DETECTION OF SCANS, Parallel Algorithms and Applications, vol.9, issue.3-4, pp.229-263, 2000.
DOI : 10.1145/318789.318810

S. Sato and H. Iwasaki, Automatic parallelization via matrix multiplication, Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation . PLDI '11, pp.470-479, 2011.
DOI : 10.1145/2345156.1993554

Y. Zou and S. Rajopadhye, Scan detection and parallelization in "inherently sequential" nested loop programs, Proceedings of the Tenth International Symposium on Code Generation and Optimization, CHO '12, pp.74-83, 2012.
DOI : 10.1145/2259016.2259027