, MISRA-C: 2004 -Guidelines for the use of the C language in critical systems, Motor Industry Software Reliability Association, 2004.
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
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.
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
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
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. ,
Proving compiler correctness in a mechanized logic, Proc. 7th Annual Machine Intelligence Workshop, pp.51-72, 1972. ,
, 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.
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. ,