{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T14:11:13Z","timestamp":1725718273989},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642368172"},{"type":"electronic","value":"9783642368189"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-36818-9_31","type":"book-chapter","created":{"date-parts":[[2013,3,4]],"date-time":"2013-03-04T16:14:54Z","timestamp":1362413694000},"page":"300-305","source":"Crossref","is-referenced-by-count":1,"title":["UVHM: Model Checking Based Formal Analysis Scheme for Hypervisors"],"prefix":"10.1007","author":[{"given":"Yuchao","family":"She","sequence":"first","affiliation":[]},{"given":"Hui","family":"Li","sequence":"additional","affiliation":[]},{"given":"Hui","family":"Zhu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"31_CR1","unstructured":"Marshall, D.: Microsoft Hyper-V gets its first security patch. Infoworld (February 2010), \n                      \n                        http:\/\/www.infoworld.com\/d\/virtualization\/microsoft-hyper-v-gets-its-first-security-patch-106"},{"key":"31_CR2","unstructured":"Vulnerability report: MS11-047 \u2013 Vulnerability in Microsoft Hyper-V could cause denial of service (June 2011), \n                      \n                        http:\/\/www.sophos.com\/support\/knowledgebase\/article\/113734.html"},{"key":"31_CR3","unstructured":"Clarke, E., Grumberg, O., Long, D.: Model Checking. MIT Press (1999)"},{"key":"31_CR4","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"key":"31_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"806","DOI":"10.1007\/978-3-642-05089-3_51","volume-title":"FM 2009: Formal Methods","author":"D. Leinenbach","year":"2009","unstructured":"Leinenbach, D., Santen, T.: Verifying the Microsoft Hyper-V Hypervisor with VCC. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 806\u2013809. Springer, Heidelberg (2009)"},{"issue":"5","key":"31_CR6","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/s10009-011-0195-9","volume":"13","author":"L. Freitas","year":"2011","unstructured":"Freitas, L., McDermott, J.: Formal methods for security in the Xenon hypervisor. International Journal on Software Tools for Technology Transfer\u00a013(5), 463\u2013489 (2011)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"31_CR7","doi-asserted-by":"crossref","unstructured":"Webster, M., Malcolm, G.: Detection of metamorphic and virtualization-based malware using algebraic specifi cation. In: EICAR 2008 (2008)","DOI":"10.1007\/s11416-008-0094-0"},{"key":"31_CR8","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley (2004)"},{"issue":"7","key":"31_CR9","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/1965724.1965743","volume":"54","author":"T. Ball","year":"2011","unstructured":"Ball, T., Levin, V., Rajamani, S.K.: A Decade of Software Model Checking with SLAM. Communications of the ACM\u00a054(7), 68\u201376 (2011)","journal-title":"Communications of the ACM"},{"issue":"5","key":"31_CR10","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/360051.360056","volume":"19","author":"D. Denning","year":"1976","unstructured":"Denning, D.: lattice model of secure information flow. Communications of the ACM\u00a019(5), 236\u2013243 (1976)","journal-title":"Communications of the ACM"},{"key":"31_CR11","doi-asserted-by":"crossref","unstructured":"Shen, J., Qing, S.: A Dynamic Information Flow Model of Secure Systems. In: CCS, pp. 341\u2013343 (2007)","DOI":"10.1145\/1229285.1229321"}],"container-title":["Lecture Notes in Computer Science","Information and Communicatiaon Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-36818-9_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,11]],"date-time":"2019-05-11T14:00:54Z","timestamp":1557583254000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-36818-9_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642368172","9783642368189"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-36818-9_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}