E. Alkassar, E. Cohen, M. Kovalev, and W. Paul, Verification of TLB Virtualization Implemented in C, 4th International Conference on Verifed Software: Theories , Tools, and Experiments, VSTTE'12, 2012.
DOI : 10.1145/1629575.1629596

S. J. Andrabi, Verification of XMHF HPT protection setup, Project_work/ VerificationofXMHFHPTProtectionSetup.pdf 4. ARM system memory management unit, 2012.

R. H. Arpaci-dusseau and A. C. Arpaci-dusseau, Operating Systems: Three Easy Pieces. Arpaci-Dusseau Books, 0, 2014.

G. Barthe, G. Betarte, J. Campo, and C. Luna, Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization, 2012 IEEE 25th Computer Security Foundations Symposium, pp.2012-2037, 2012.
DOI : 10.1109/CSF.2012.17

A. Blanchard, N. Kosmatov, M. Lemerre, and F. Loulergue, A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C, FMICS 2015 Proceedings, pp.15-30978, 2015.
DOI : 10.1007/978-3-319-19458-5_2

E. Cohen, M. Dahlweid, M. A. Hillebrand, D. Leinenbach, M. Moskal et al., VCC: A Practical System for Verifying Concurrent C, Theorem Proving in Higher Order Logics, 22nd International Conference, pp.23-42, 2009.
DOI : 10.1007/978-3-540-74591-4_15

M. Daum, N. Billing, and G. Klein, Concerned with the unprivileged: user programs in kernel refinement, Formal Aspects of Computing, vol.34, issue.1, pp.1205-1229, 2014.
DOI : 10.1007/s00165-014-0296-9

M. Kovalev, TLB virtualization in the context of hypervisor verification, pp.66041-5215, 2013.

S. Lescuyer, ProvenCore: Towards a verified isolation micro-kernel In: International Workshop on MILS: Architecture and Assurance for Secure Systems, 2015.

R. Mijat and A. Nightingale, Virtualization is coming to a platform near you (2011), https://www.arm.com/files

T. C. Murray, D. Matichuk, M. Brassil, P. Gammie, T. Bourke et al., seL4: From General Purpose to a Proof of Information Flow Enforcement, 2013 IEEE Symposium on Security and Privacy, pp.415-429, 2013.
DOI : 10.1109/SP.2013.35

H. Nemati, R. Guanciale, and M. Dam, Trustworthy Virtualization of the ARMv7 Memory Subsystem, SOFSEM 2015: Theory and Practice of Computer Science -41st International Conference on Current Trends in Theory and Practice of Computer Science Proceedings. pp, pp.578-589978, 2015.
DOI : 10.1007/978-3-662-46078-8_48

A. Vasudevan, S. Chaki, L. Jia, J. Mccune, J. Newsome et al., Design, Implementation and Verification of an eXtensible and Modular Hypervisor Framework, 2013 IEEE Symposium on Security and Privacy, pp.430-444, 2013.
DOI : 10.1109/SP.2013.36

J. Vetter, M. Petschik-junker, J. Nordholz, M. Peter, and J. Danisevskis, Uncloaking Rootkits on Mobile Devices with a Hypervisor-Based Detector, ICISC (International Conference on Information Security and Cryptology), 2015.
DOI : 10.1007/978-3-319-30840-1_17