, MISRA-C: 2004 -Guidelines for the use of the C language in critical systems, Motor Industry Software Reliability Association, 2004.

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development -Coq'Art: The Calculus of Inductive Constructions, EATCS Texts in Theoretical Computer Science, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

E. Eide and J. Regehr, Volatiles are miscompiled, and what to do about it, Proceedings of the 8th ACM & IEEE International conference on Embedded software, pp.255-264, 2008.

, AbsInt Angewandte Informatik GmbH. AbsInt Advanced Analyzer

, International standard ISO/IEC 9899:1999, Programming languages -C, 1999.

, ISO. International standard ISO/IEC 9899:2011, Programming languages -C, 2011.

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

X. Leroy, A formally verified compiler back-end, Journal of Automated Reasoning, vol.43, issue.4, pp.363-446, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00360768

J. Mccarthy and J. Painter, Correctness of a compiler for arithmetical expressions, Mathematical Aspects of Computer Science, volume 19 of Proc. of Symposia in Applied Mathematics, pp.33-41, 1967.

R. Milner and . Weyrauch, Proving compiler correctness in a mechanized logic, Proc. 7th Annual Machine Intelligence Workshop, pp.51-72, 1972.

C. Benjamin, A. Pierce, C. Azevedo-de-amorim, M. Casinghino, M. Gaboardi et al., C?t?lin Hri?cu, Vilhelm Sjöberg, and Brent Yorgey. Software Foundations. Electronic textbook, 2017.

, IEEE standard for floating-point arithmetic, IEEE Computer Society, pp.754-2008, 2008.

X. Yang, Y. Chen, E. Eide, and J. Regehr, Finding and understanding bugs in C compilers, Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp.283-294, 2011.