Previous Up

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]
ISO. International standard ISO/IEC 9899:1999, Programming languages – C, 1999.
[5]
ISO. International standard ISO/IEC 9899:2011, Programming languages – C, 2011.
[6]
Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107–115, 2009.
[7]
Xavier Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363–446, 2009.
[8]
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.
[9]
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.
[10]
IEEE Computer Society. IEEE standard for floating-point arithmetic, IEEE Std 754-2008, 2008.
[11]
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.

Previous Up