References

[1]

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

[2]

Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development – Coq’Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science. Springer, 2004.

[3]

Eric Eide and John Regehr. Volatiles are miscompiled, and what to do about it. In Proceedings of the 8th ACM & IEEE International conference on Embedded software, EMSOFT 2008, pages 255–264. ACM Press, 2008.

[4]

AbsInt Angewandte Informatik GmbH. AbsInt Advanced Analyzer. Saarbrücken, Germany. User Documentation.

[5]

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

[6]

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

[7]

Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107–115, 2009.

[8]

Xavier Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363–446, 2009.

[9]

John McCarthy and James Painter. Correctness of a compiler for arithmetical expressions. In Mathematical Aspects of Computer Science, volume 19 of Proc. of Symposia in Applied Mathematics, pages 33–41. American Mathematical Society, 1967.

[10]

R[obin] Milner and R[ichard] Weyrauch. Proving compiler correctness in a mechanized logic. In Bernard Meltzer and Donald Michie, editors, Proc. 7th Annual Machine Intelligence Workshop, volume 7 of Machine Intelligence, pages 51–72. Edinburgh University Press, 1972.

[11]

Benjamin C. Pierce et al. Software Foundations. Electronic textbook, 2021. Version 6.1. https://softwarefoundations.cis.upenn.edu/.

[12]

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

[13]

Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. Finding and understanding bugs in C compilers. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pages 283–294. ACM Press, 2011.