{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:18:20Z","timestamp":1725455900553},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642351815"},{"type":"electronic","value":"9783642351822"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-35182-2_22","type":"book-chapter","created":{"date-parts":[[2012,12,6]],"date-time":"2012-12-06T01:19:15Z","timestamp":1354756755000},"page":"312-314","source":"Crossref","is-referenced-by-count":0,"title":["Scalable Formal Machine Models"],"prefix":"10.1007","author":[{"given":"Greg","family":"Morrisett","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"Milner, R., Weyhrauch, R.: Proving compiler correctness in a mechanized logic. In: Proceedings of the 7th Annual Machine Intelligence Workshop. Machine Intelligence, vol.\u00a07, pp. 51\u201372. Edinburgh University Press (1972)"},{"issue":"7","key":"22_CR2","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. of the ACM\u00a052(7), 107\u2013115 (2009)","journal-title":"Commun. of the ACM"},{"key":"22_CR3","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1145\/1629575.1629596","volume-title":"Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, SOSP 2009","author":"G. Klein","year":"2009","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 ACM SIGOPS 22nd Symposium on Operating Systems Principles, SOSP 2009, pp. 207\u2013220. ACM, New York (2009)"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Wahbe, R., Lucco, S., Anderson, T.E., Graham, S.L.: Efficient software-based fault isolation. In: Proc. of the 14th ACM Symp. on Operating Systems Principles, SOSP 1993, pp. 203\u2013216. ACM (1993)","DOI":"10.1145\/173668.168635"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Abadi, M., Budiu, M., Erlingsson, U., Ligatti, J.: Control-flow integrity. In: Proc. of the 12th ACM Conf. on Computer and Commun. Security, CCS 2005, pp. 340\u2013353. ACM (2005)","DOI":"10.1145\/1102120.1102165"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. In: Proc. of the 25th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL 1998, pp. 85\u201397. ACM (1998)","DOI":"10.1145\/268946.268954"},{"issue":"3","key":"22_CR7","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1145\/256167.256225","volume":"19","author":"N. Ramsey","year":"1997","unstructured":"Ramsey, N., Fernandez, M.F.: Specifying representations of machine instructions. ACM Trans. Program. Lang. Syst.\u00a019(3), 492\u2013524 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BFb0057790","volume-title":"Languages, Compilers, and Tools for Embedded Systems","author":"N. Ramsey","year":"1998","unstructured":"Ramsey, N., Davidson, J.W.: Machine Descriptions to Build Tools for Embedded Systems. In: M\u00fcller, F., Bestavros, A. (eds.) LCTES 1998. LNCS, vol.\u00a01474, pp. 176\u2013192. Springer, Heidelberg (1998)"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Dias, J., Ramsey, N.: Automatically generating instruction selectors using declarative machine descriptions. In: Proc. of the 37th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL 2010, pp. 403\u2013416. ACM (2010)","DOI":"10.1145\/1706299.1706346"},{"key":"22_CR10","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1145\/2254064.2254111","volume-title":"Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2012","author":"G. Morrisett","year":"2012","unstructured":"Morrisett, G., Tan, G., Tassarotti, J., Tristan, J.B., Gan, E.: Rocksalt: better, faster, stronger sfi for the x86. In: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2012, pp. 395\u2013404. ACM, New York (2012)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35182-2_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,9]],"date-time":"2019-05-09T18:51:15Z","timestamp":1557427875000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35182-2_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642351815","9783642351822"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35182-2_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}