{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T00:50:30Z","timestamp":1742950230518,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319194578"},{"type":"electronic","value":"9783319194585"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-19458-5_2","type":"book-chapter","created":{"date-parts":[[2015,5,11]],"date-time":"2015-05-11T11:41:14Z","timestamp":1431344474000},"page":"15-30","source":"Crossref","is-referenced-by-count":16,"title":["A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C"],"prefix":"10.1007","author":[{"given":"Allan","family":"Blanchard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nikolai","family":"Kosmatov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthieu","family":"Lemerre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fr\u00e9d\u00e9eric","family":"Loulergue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"2_CR1","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. Journal of Automated Reasoning\u00a043(4), 363\u2013446 (2009)","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Verified squared: does critical software deserve verified tools? In: POPL 2011. ACM (2011)","DOI":"10.1145\/1926385.1926387"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Murray, T.C., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1) (2014)","DOI":"10.1145\/2560537"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Lemerre, M., David, V., Vidal-Naquet, G.: A communication mechanism for resource isolation. In: IIES 2009 (2009)","DOI":"10.1145\/1519130.1519131"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Lemerre, M., Ohayon, E., Chabrol, D., Jan, M., Jacques, M.B.: Method and Tools for Mixed-Criticality Real-Time Applications within PharOS. In: AMICS 2011 (2011)","DOI":"10.1109\/ISORCW.2011.15"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P. Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: A software analysis perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol.\u00a07504, pp. 233\u2013247. Springer, Heidelberg (2012)"},{"key":"2_CR7","unstructured":"Baudin, P., Cuoq, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C Specification Language, \n                        http:\/\/frama-c.cea.fr\/acsl.html"},{"key":"2_CR8","unstructured":"The Coq Development Team: The Coq Proof Assistant, \n                        http:\/\/coq.inria.fr"},{"key":"2_CR9","unstructured":"Lemerre, M., David, V., Vidal-Naquet, G.: A dependable kernel design for resource isolation and protection. In: IIDS 2010 (2010)"},{"issue":"12","key":"2_CR10","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"S.V. Adve","year":"1996","unstructured":"Adve, S.V., Gharachorloo, K.: Shared memory consistency models: A tutorial. IEEE Computer\u00a029(12), 66\u201376 (1996)","journal-title":"IEEE Computer"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Saraswat, V.A., Jagadeesan, R., Michael, M.M., von Praun, C.: A theory of memory models. In: PPoPP, pp. 161\u2013172. ACM (2007)","DOI":"10.1145\/1229428.1229469"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Boudol, G., Petri, G.: Relaxed memory models: an operational approach. In: POPL 2009 (2009)","DOI":"10.1145\/1480881.1480930"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-642-03359-9_16","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Dabrowski","year":"2009","unstructured":"Dabrowski, F., Pichardie, D.: A Certified Data Race Analysis for a Java-like Language. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 212\u2013227. Springer, Heidelberg (2009)"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/978-3-642-14052-5_28","volume-title":"Interactive Theorem Proving","author":"E. Cohen","year":"2010","unstructured":"Cohen, E., Schirmer, B.: From total store order to sequential consistency: A practical reduction theorem. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 403\u2013418. Springer, Heidelberg (2010)"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-28644-8_2","volume-title":"CONCUR 2004 - Concurrency Theory","author":"S.D. Brookes","year":"2004","unstructured":"Brookes, S.D.: A semantics for concurrent separation logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 16\u201334. Springer, Heidelberg (2004)"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-15057-9_5","volume-title":"Verified Software: Theories, Tools, Experiments","author":"E. Alkassar","year":"2010","unstructured":"Alkassar, E., Paul, W.J., Starostin, A., Tsyban, A.: Pervasive verification of an OS microkernel. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol.\u00a06217, pp. 71\u201385. Springer, Heidelberg (2010)"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-642-35308-6_13","volume-title":"Certified Programs and Proofs","author":"A. Vaynberg","year":"2012","unstructured":"Vaynberg, A., Shao, Z.: Compositional verification of a baby virtual memory manager. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol.\u00a07679, pp. 143\u2013159. Springer, Heidelberg (2012)"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Barthe, G., Betarte, G., Campo, J.D., Chimento, J.M., Luna, C.: Formally verified implementation of an idealized model of virtualization. In: TYPES 2013(2013)","DOI":"10.1109\/CSF.2012.17"},{"key":"2_CR19","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., 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)"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-27705-4_17","volume-title":"Verified Software: Theories, Tools, Experiments","author":"E. Alkassar","year":"2012","unstructured":"Alkassar, E., Cohen, E., Kovalev, M., Paul, W.J.: Verification of TLB virtualization implemented in C. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 209\u2013224. Springer, Heidelberg (2012)"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Chen, G., Cohen, E., Kovalev, M.: Store buffer reduction with MMUs: Complete paper-and-pencil proof. Technical report, Saarland University, Saarbr\u00fccken (2013)","DOI":"10.1007\/978-3-319-12154-3_8"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-17164-2_3","volume-title":"Programming Languages and Systems","author":"G. Klein","year":"2010","unstructured":"Klein, G.: From a verified kernel towards verified systems. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol.\u00a06461, pp. 21\u201333. Springer, Heidelberg (2010)"},{"key":"2_CR23","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.\u00a08570, pp. 158\u2013164. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-19458-5_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T01:51:06Z","timestamp":1676944266000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-19458-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319194578","9783319194585"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-19458-5_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}