X. Leroy, A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, pp.363-446, 2009.
DOI : 10.1007/978-3-642-59495-3
URL : https://hal.archives-ouvertes.fr/inria-00360768

X. Leroy, Verified squared: does critical software deserve verified tools? In: POPL, 2011.

G. Klein, J. Andronick, K. Elphinstone, T. C. Murray, T. Sewell et al., Comprehensive formal verification of an OS microkernel, ACM Transactions on Computer Systems, vol.32, issue.1, 2014.
DOI : 10.1145/355616.364017

M. Lemerre, V. David, and G. Vidal-naquet, A communication mechanism for resource isolation, Proceedings of the Second Workshop on Isolation and Integration in Embedded Systems, IIES '09, 2009.
DOI : 10.1145/1519130.1519131
URL : https://hal.archives-ouvertes.fr/hal-00471460

M. Lemerre, E. Ohayon, D. Chabrol, M. Jan, and M. B. Jacques, Method and Tools for Mixed-Criticality Real-Time Applications within PharOS, 2011 14th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing Workshops, 2011.
DOI : 10.1109/ISORCW.2011.15

P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles et al., Frama-C, p.2012
DOI : 10.1007/978-3-642-33826-7_16

P. Baudin, P. Cuoq, J. C. Filliâtre, C. Marché, B. Monate et al., ACSL: ANSI/ISO C Specification Language

, The Coq Development Team: The Coq Proof Assistant

M. Lemerre, V. David, and G. Vidal-naquet, A dependable kernel design for resource isolation and protection, p.2010
URL : https://hal.archives-ouvertes.fr/hal-00517703

S. V. Adve and K. Gharachorloo, Shared memory consistency models: a tutorial, Computer, vol.29, issue.12, pp.66-76, 1996.
DOI : 10.1109/2.546611

V. A. Saraswat, R. Jagadeesan, M. M. Michael, and C. Von-praun, A theory of memory models, Proceedings of the 12th ACM SIGPLAN symposium on Principles and practice of parallel programming , PPoPP '07, pp.161-172, 2007.
DOI : 10.1145/1229428.1229469

G. Boudol and G. Petri, Relaxed memory models: an operational approach, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00420352

F. Dabrowski and D. Pichardie, A Certified Data Race Analysis for a Java-like Language, 2009.
DOI : 10.1145/1146809.1146811
URL : https://hal.archives-ouvertes.fr/hal-00465547

E. Cohen and B. Schirmer, From Total Store Order to Sequential Consistency: A Practical Reduction Theorem, 2010.
DOI : 10.1007/978-3-642-14052-5_28

S. D. Brookes, A semantics for concurrent separation logic, 2004.

E. Alkassar, W. Paul, A. Starostin, and A. Tsyban, Pervasive Verification of an OS Microkernel, 2010.
DOI : 10.1007/978-3-642-15057-9_5

A. Vaynberg and Z. Shao, Compositional Verification of a Baby Virtual Memory Manager, p.2012
DOI : 10.1007/978-3-642-35308-6_13

G. Barthe, G. Betarte, J. D. Campo, J. M. Chimento, and C. Luna, Formally verified implementation of an idealized model of virtualization, p.2013

E. Alkassar, M. A. Hillebrand, W. J. Paul, and E. Petrova, Automated Verification of a Small Hypervisor, 2010.
DOI : 10.1007/978-3-642-15057-9_3

E. Alkassar, E. Cohen, M. Kovalev, and W. J. Paul, Verification of TLB Virtualization Implemented in C, p.2012
DOI : 10.1145/1629575.1629596

G. Chen, E. Cohen, and M. Kovalev, Store Buffer Reduction with MMUs, 2013.
DOI : 10.1007/978-3-319-12154-3_8

G. Klein, From a Verified Kernel towards Verified Systems, p.2010
DOI : 10.1145/1806596.1806610

N. Kosmatov, M. Lemerre, and C. Alec, A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing, p.2014
DOI : 10.1007/978-3-319-09099-3_12
URL : https://hal.archives-ouvertes.fr/cea-01822965