{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T18:19:55Z","timestamp":1763057995356,"version":"3.41.0"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319489889"},{"type":"electronic","value":"9783319489896"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-48989-6_5","type":"book-chapter","created":{"date-parts":[[2016,11,7]],"date-time":"2016-11-07T06:31:19Z","timestamp":1478500279000},"page":"69-84","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor"],"prefix":"10.1007","author":[{"given":"Hanno","family":"Becker","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Juan Manuel","family":"Crespo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacek","family":"Galowicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ulrich","family":"Hensel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yoichi","family":"Hirai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C\u00e9sar","family":"Kunz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Keiko","family":"Nakata","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jorge Luis","family":"Sacchini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hendrik","family":"Tews","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Tuerk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,11,8]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-642-21437-0_19","volume-title":"FM 2011: Formal Methods","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Betarte, G., Campo, J.D., Luna, C.: Formally verifying isolation and availability in an idealized model of virtualization. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 231\u2013245. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-21437-0_19"},{"issue":"2\u20133","key":"5_CR2","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1561\/2500000002","volume":"2","author":"J Bertrane","year":"2015","unstructured":"Bertrane, J., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Rival, X.: Static analysis and verification of aerospace software by abstract interpretation. Found. Trends Program. Lang. 2(2\u20133), 71\u2013190 (2015)","journal-title":"Found. Trends Program. Lang."},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-319-19249-9_20","volume-title":"FM 2015: Formal Methods","author":"G Brat","year":"2015","unstructured":"Brat, G., Bushnell, D., Davies, M., Giannakopoulou, D., Howar, F., Kahsai, T.: Verifying the safety of a flight-critical system. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 308\u2013324. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-19249-9_20"},{"issue":"5","key":"5_CR4","doi-asserted-by":"publisher","first-page":"683","DOI":"10.1007\/s00165-012-0222-y","volume":"25","author":"AD Brucker","year":"2013","unstructured":"Brucker, A.D., Wolff, B.: On theorem prover-based testing. Formal Aspects Comput. 25(5), 683\u2013721 (2013)","journal-title":"Formal Aspects Comput."},{"key":"5_CR5","unstructured":"Cai, H., Shao, Z., Vaynberg, A.: Certified self-modifying code. In: Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10\u201313, 2007, pp. 66\u201377 (2007)"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-17524-9_1","volume-title":"NASA Formal Methods","author":"C Calcagno","year":"2015","unstructured":"Calcagno, C., et al.: Moving fast with software verification. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 3\u201311. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-17524-9_1"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Elphinstone, K., Heiser, G.: From L3 to seL4 - what have we learnt in 20 years of L4 microkernels? In: Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles, SOSP 2013, pp. 133\u2013150. ACM, New York (2013)","DOI":"10.1145\/2517349.2522720"},{"key":"5_CR8","unstructured":"Feng, X., Shao, Z., Dong, Y., Guo, Y.: Certifying low-level programs with hardware interrupts and preemptive threads. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7\u201313, 2008, pp. 170\u2013182 (2008)"},{"key":"5_CR9","unstructured":"Gu, L., Vaynberg, A., Ford, B., Shao, Z., Costanzo, D.: Certikos: a certified kernel for secure cloud computing. In: APSys 2011 Asia Pacific Workshop on Systems, Shanghai, China, July 11-12, 2011, p. 3 (2011)"},{"key":"5_CR10","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: Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, SOSP 2009, Big Sky, Montana, USA, October 11\u201314, 2009, pp. 207\u2013220 (2009)"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-319-09099-3_12","volume-title":"Tests and Proofs","author":"N Kosmatov","year":"2014","unstructured":"Kosmatov, N., Lemerre, M., Alec, C.: A case study on verification of a cloud hypervisor by proof and structural testing. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 158\u2013164. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-09099-3_12"},{"issue":"4","key":"5_CR12","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Autom. Reasoning 43(4), 363\u2013446 (2009)","journal-title":"J. Autom. Reasoning"},{"issue":"9","key":"5_CR13","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1145\/234215.234473","volume":"39","author":"J Liedtke","year":"1996","unstructured":"Liedtke, J.: Toward real $${\\mu }$$ \u03bc -kernels. Commun. ACM 39(9), 70\u201377 (1996)","journal-title":"Commun. ACM"},{"issue":"3","key":"5_CR14","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1145\/322017.322025","volume":"24","author":"RJ Lipton","year":"1977","unstructured":"Lipton, R.J., Snyder, L.: A linear time algorithm for deciding subject security. J. ACM 24(3), 455\u2013464 (1977)","journal-title":"J. ACM"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/978-3-319-19249-9_39","volume-title":"FM 2015: Formal Methods","author":"T Liu","year":"2015","unstructured":"Liu, T., Huuck, R.: Case study: static security analysis of the android goldfish kernel. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 589\u2013592. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-19249-9_39"},{"key":"5_CR16","unstructured":"Murray, T.C., Matichuk, D., Brassil, M., Gammie, P., Bourke, T., Seefried, S., Lewis, C., Gao, X., Klein, G.: sel4: from general purpose to a proof of information flow enforcement. In: 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19\u201322, 2013, pp. 415\u2013429 (2013)"},{"issue":"4","key":"5_CR17","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/2699417","volume":"58","author":"C Newcombe","year":"2015","unstructured":"Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How amazon web services uses formal methods. Commun. ACM 58(4), 66\u201373 (2015)","journal-title":"Commun. ACM"},{"key":"5_CR18","unstructured":"Ramananandro, T., Reis, G.D., Leroy, X.: Formal verification of object layout for c++ multiple inheritance. In: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26\u201328, 2011, pp. 67\u201380 (2011)"},{"key":"5_CR19","unstructured":"Ramananandro, T., Reis, G.D., Leroy, X.: A mechanized semantics for C++ object construction and destruction, with applications to resource management. In: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22\u201328, 2012, pp. 521\u2013532 (2012)"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-642-22863-6_24","volume-title":"Interactive Theorem Proving","author":"T Sewell","year":"2011","unstructured":"Sewell, T., Winwood, S., Gammie, P., Murray, T., Andronick, J., Klein, G.: seL4 enforces integrity. In: Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 325\u2013340. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22863-6_24"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Shao, Z.: Clean-slate development of certified OS kernels. In: Proceedings of the 2015 Conference on Certified Programs and Proofs, Cp. 2015, Mumbai, India, January 15\u201317, 2015, pp. 95\u201396 (2015)","DOI":"10.1145\/2676724.2693180"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Shapiro, J.S., Weber, S.: Verifying the eros confinement mechanism. In: Proceedings of the 2000 IEEE Symposium on Security and Privacy, SP 2000, p. 166. IEEE Computer Society, Washington, DC (2000)","DOI":"10.1109\/SECPRI.2000.848454"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Steinberg, U., Kauer, B.: Nova: a microhypervisor-based secure virtualization architecture. In: Proceedings of the 5th European Conference on Computer Systems, EuroSys 2010, pp. 209\u2013222. ACM, New York (2010)","DOI":"10.1145\/1755913.1755935"},{"key":"5_CR24","unstructured":"FireEye Formal Methods Team. Efficiently executable sets used by FireEye. Presented at the 8th Coq Workshop (2016). https:\/\/github.com\/fireeye\/MSetsExtra"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1007\/978-3-319-06410-9_49","volume-title":"FM 2014: Formal Methods","author":"H Zhao","year":"2014","unstructured":"Zhao, H., Yang, M., Zhan, N., Gu, B., Zou, L., Chen, Y.: Formal verification of a descent guidance control program of a lunar lander. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 733\u2013748. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-06410-9_49"}],"container-title":["Lecture Notes in Computer Science","FM 2016: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-48989-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T01:24:42Z","timestamp":1749691482000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-48989-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319489889","9783319489896"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-48989-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"8 November 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Limassol","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cyprus","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 November 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 November 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/fm2016.cs.ucy.ac.cy\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}