D. Marshall, Microsoft Hyper-V gets its first security patch Infoworld, Feb, 2010.

C. Baier and J. P. Katoen, Principles of Model Checking, 2008.

D. Leinenbach and T. Santen, Verifying the Microsoft Hyper-V Hypervisor with VCC, LNCS, vol.5850, pp.806-809, 2009.
DOI : 10.1007/978-3-642-05089-3_51

L. Freitas and J. Mcdermott, Formal methods for security in the Xenon hypervisor, International Journal on Software Tools for Technology Transfer, vol.21, issue.1, pp.463-489, 2011.
DOI : 10.1007/s10009-011-0195-9

M. Webster and G. Malcolm, Detection of metamorphic and virtualization-based malware using algebraic specifi cation, Proc. EICAR, 2008.

J. Gerard and . Holzmann, The SPIN Model Checker: Primer and Reference Manual, 2004.

T. Ball, V. Levin, and S. K. Rajamani, A decade of software model checking with SLAM, Communications of the ACM, vol.54, issue.7, pp.68-76, 2011.
DOI : 10.1145/1965724.1965743

D. Denning, A lattice model of secure information flow, Communications of the ACM, vol.19, issue.5, pp.236-243, 1976.
DOI : 10.1145/360051.360056

J. Shen and S. Qing, A dynamic information flow model of secure systems, Proceedings of the 2nd ACM symposium on Information, computer and communications security , ASIACCS '07, pp.341-343, 2007.
DOI : 10.1145/1229285.1229321