{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T17:07:34Z","timestamp":1725815254230},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662460771"},{"type":"electronic","value":"9783662460788"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46078-8_48","type":"book-chapter","created":{"date-parts":[[2015,1,14]],"date-time":"2015-01-14T09:54:29Z","timestamp":1421229269000},"page":"578-589","source":"Crossref","is-referenced-by-count":14,"title":["Trustworthy Virtualization of the ARMv7 Memory Subsystem"],"prefix":"10.1007","author":[{"given":"Hamed","family":"Nemati","sequence":"first","affiliation":[]},{"given":"Roberto","family":"Guanciale","sequence":"additional","affiliation":[]},{"given":"Mads","family":"Dam","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"48_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-642-15057-9_3","volume-title":"Verified Software: Theories, Tools, Experiments","author":"E. Alkassar","year":"2010","unstructured":"Alkassar, E., Hillebrand, M.A., Paul, W.J., Petrova, E.: Automated verification of a small hypervisor. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol.\u00a06217, pp. 40\u201354. Springer, Heidelberg (2010)"},{"unstructured":"ARMv7-A architecture reference manual, \n                    \n                      http:\/\/infocenter.arm.com\/help\/index.jsp?topic=\/com.arm.doc.ddi0406b","key":"48_CR2"},{"key":"48_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-14052-5_18","volume-title":"Interactive Theorem Proving","author":"A. Fox","year":"2010","unstructured":"Fox, A., Myreen, M.O.: A trustworthy monadic formalization of the aRMv7 instruction set architecture. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 243\u2013258. Springer, Heidelberg (2010)"},{"doi-asserted-by":"crossref","unstructured":"Heiser, G., Leslie, B.: The OKL4 microvisor: convergence point of microkernels and hypervisors. In: Thekkath, C.A., Kotla, R. and Zhou, L. (eds.), ApSys, pp. 19\u201324. ACM (2010)","key":"48_CR4","DOI":"10.1145\/1851276.1851282"},{"issue":"1","key":"48_CR5","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1109\/TSE.2007.70772","volume":"34","author":"C. Heitmeyer","year":"2008","unstructured":"Heitmeyer, C., Archer, M., Leonard, E., McLean, J.: Applying formal methods to a certifiably secure software system. IEEE Trans. Softw. Eng.\u00a034(1), 82\u201398 (2008)","journal-title":"IEEE Trans. Softw. Eng."},{"doi-asserted-by":"crossref","unstructured":"Hwang, J.-Y., Suh, S.-B., Heo, S.-K., Park, C.-J., Ryu, J.-M., Park, S.-Y., Kim, C.-R.: Xen on ARM: System virtualization using Xen hypervisor for ARM-based secure mobile phones. In: 5th IEEE Consumer Communications and Networking Conference, CCNC 2008, pp. 257\u2013261. IEEE (2008)","key":"48_CR6","DOI":"10.1109\/ccnc08.2007.64"},{"unstructured":"Iqbal, A., Sadeque, N., Mutia, R.I.: An overview of microkernel, hypervisor and microvisor virtualization approaches for embedded systems. Report, Department of Electrical and Information Technology, Lund University, Sweden, 2110 (2009)","key":"48_CR7"},{"key":"48_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-319-03545-1_18","volume-title":"Certified Programs and Proofs","author":"N. Khakpour","year":"2013","unstructured":"Khakpour, N., Schwarz, O., Dam, M.: Machine assisted proof of aRMv7 instruction level isolation properties. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol.\u00a08307, pp. 276\u2013291. Springer, Heidelberg (2013)"},{"doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an OS kernel. In: Matthews, J.N., Anderson, T.E. (eds.), SOSP, pp. 207\u2013220. ACM (2009)","key":"48_CR9","DOI":"10.1145\/1629575.1629596"},{"key":"48_CR10","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)"},{"doi-asserted-by":"crossref","unstructured":"McCoyd, M., Krug, R.B., Goel, D., Dahlin, M., Young, W.D.: Building a hypervisor on a formally verifiable protection layer. In: HICSS, pp. 5069\u20135078. IEEE (2013)","key":"48_CR11","DOI":"10.1109\/HICSS.2013.121"},{"doi-asserted-by":"crossref","unstructured":"Sewell, T.A.L., Myreen, M.O., Klein, G.: Translation validation for a verified os kernel. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 471\u2013482. ACM (2013)","key":"48_CR12","DOI":"10.1145\/2491956.2462183"}],"container-title":["Lecture Notes in Computer Science","SOFSEM 2015: Theory and Practice of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46078-8_48","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T23:59:22Z","timestamp":1559087962000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46078-8_48"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662460771","9783662460788"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46078-8_48","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}