C. Bastoul, Generating loops for scanning polyhedra, 2002.

F. Besson, Fast Reflexive Arithmetic Tactics the Linear Case and Beyond, Types for Proofs and Programs, pp.48-62
DOI : 10.1007/978-3-540-74464-1_4

U. Bondhugula, A. Hartono, J. Ramanujam, and P. P. Sadayappan, Pluto: A practical and fully automatic polyhedral program optimization system, In: Proceedings of the ACM SIGPLAN, 2008.

T. Grosser, Enabling polyhedral optimizations in llvm, 2011.

A. Kanade, A. Sanyal, and U. P. Khedker, A PVS Based Framework for Validating Compiler Optimizations, Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06), pp.108-117, 2006.
DOI : 10.1109/SEFM.2006.4

X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, 2009.
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861

X. Leroy, The Compcert verified compiler, software and commented proof, 2010.

J. L. Lions, Ariane 5 -flight 501 failure, 1996.

G. C. Necula, Translation validation for an optimizing compiler, ACM SIGPLAN Notices, vol.35, issue.5, pp.83-94, 2000.
DOI : 10.1145/358438.349314

A. Pnueli, M. Siegel, and E. Singerman, Translation validation, Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, pp.151-166, 1998.
DOI : 10.1007/BFb0054170

. Polylib, u-strasbg.fr/PolyLib. [13] PPL: The parma polyhedra library

K. Trifunovic, A. Cohen, D. Edelsohn, F. Li, T. Grosser et al., GRAPHITE Two Years After: First Lessons Learned From Real-World Polyhedral Compilation, GCC Research Opportunities Workshop (GROW'10), 2010.
URL : https://hal.archives-ouvertes.fr/inria-00551516

J. Tristan, Formal verification of translation validators. These, 2009.
URL : https://hal.archives-ouvertes.fr/tel-00437582

J. Tristan and X. Leroy, Formal verification of translation validators: A case study on instruction scheduling optimizations, 35th ACM Symposium on Principles of Programming Languages, pp.17-27, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00289540

J. Tristan and X. Leroy, Verified Validation of Lazy Code Motion, ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI), pp.316-326, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00415865

J. Tristan and X. Leroy, A simple, verified validator for software pipelining, 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00529836

S. Verdoolaege, barvinok: User Guide, 2011.

S. Verdoolaege, R. Seghir, K. Beyls, V. Loechner, and M. Bruynooghe, Counting Integer Points in Parametric Polytopes Using Barvinok's Rational Functions, Algorithmica, vol.48, issue.1, pp.37-66, 2007.
DOI : 10.1007/s00453-006-1231-0

L. Zuck, A. Pnueli, Y. Fang, B. Goldberg, and Y. Hu, Translation and run-time validation of optimized code, 2nd Workshop on Runtime Verification, pp.180-201, 2002.