{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,27]],"date-time":"2026-10-27T01:11:32Z","timestamp":1793063492802,"version":"4.5.0"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2011,10,9]],"date-time":"2011-10-09T00:00:00Z","timestamp":1318118400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2011,10,9]]},"DOI":"10.1145\/2038642.2038687","type":"proceedings-article","created":{"date-parts":[[2011,10,11]],"date-time":"2011-10-11T14:29:11Z","timestamp":1318343351000},"page":"289-298","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":53,"title":["ARMor"],"prefix":"10.1145","author":[{"given":"Lu","family":"Zhao","sequence":"first","affiliation":[{"name":"University of Utah, Salt Lake City, UT, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Guodong","family":"Li","sequence":"additional","affiliation":[{"name":"Fujitsu Laboratories of America, Sunnyvale, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bjorn","family":"De Sutter","sequence":"additional","affiliation":[{"name":"Ghent University, Ghent, Belgium"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"John","family":"Regehr","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, UT, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2011,10,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1102120.1102165"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11576280_9"},{"key":"e_1_3_2_1_3_1","unstructured":"C. L. Biffle. Undefined behavior in Google NaCl. http:\/\/code.google.com\/p\/nativeclient\/issues\/detail?id=245.  C. L. Biffle. Undefined behavior in Google NaCl. http:\/\/code.google.com\/p\/nativeclient\/issues\/detail?id=245."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/227595.227603"},{"key":"e_1_3_2_1_5_1","volume-title":"Symp. on Operating Systems Design and Implementation (OSDI)","author":"Abadi M.","year":"2006","unstructured":"\u00da. Erlingsson, M. Abadi , M. Vrable , M. Budiu , and G. C. Necula . XFI: Software guards for system address spaces . In Symp. on Operating Systems Design and Implementation (OSDI) , 2006 . \u00da. Erlingsson, M. Abadi, M. Vrable, M. Budiu, and G. C. Necula. XFI: Software guards for system address spaces. In Symp. on Operating Systems Design and Implementation (OSDI), 2006."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_2"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_18"},{"key":"e_1_3_2_1_9_1","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","author":"Gordon M. J. C.","year":"1993","unstructured":"M. J. C. Gordon and T. F. Melham , editors . Introduction to HOL: A Theorem Proving Environment for Higher Order Logic . Cambridge University Press , 1993 . M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1128020.1128563"},{"key":"e_1_3_2_1_12_1","volume-title":"Proc. of the 15th USENIX Security Symp.","author":"McCamant S.","year":"2006","unstructured":"S. McCamant and G. Morrisett . Evaluating SFI for a CISC architecture . In Proc. of the 15th USENIX Security Symp. , Aug. 2006 . S. McCamant and G. Morrisett. Evaluating SFI for a CISC architecture. In Proc. of the 15th USENIX Security Symp., Aug. 2006."},{"key":"e_1_3_2_1_13_1","first-page":"350","volume-title":"Proc. of the 1991 Intl. Workshop on the HOL Theorem Proving System and its Applications","author":"Melham T. F.","year":"1992","unstructured":"T. F. Melham . A package for inductive relation definitions in HOL . In Proc. of the 1991 Intl. Workshop on the HOL Theorem Proving System and its Applications , pages 350 -- 357 , 1992 . T. F. Melham. A package for inductive relation definitions in HOL. In Proc. of the 1991 Intl. Workshop on the HOL Theorem Proving System and its Applications, pages 350--357, 1992."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1775223.1775241"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763507.1763565"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1517424.1517444"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111066"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1929820.1929822"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-40018-9_16"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_6"},{"key":"e_1_3_2_1_23_1","first-page":"7","volume-title":"Proc. of the 2005 IEEE International Symposium On Signal Processing And Information Technology","author":"Put L. Van","year":"2005","unstructured":"L. Van Put , D. Chanet , B. De Bus , B. De Sutter , and K. De Bosschere . Diablo: A reliable, retargetable and extensible link-time rewriting framework . In Proc. of the 2005 IEEE International Symposium On Signal Processing And Information Technology , pages 7 -- 12 , Athens, 12 2005 . L. Van Put, D. Chanet, B. De Bus, B. De Sutter, and K. De Bosschere. Diablo: A reliable, retargetable and extensible link-time rewriting framework. In Proc. of the 2005 IEEE International Symposium On Signal Processing And Information Technology, pages 7--12, Athens, 12 2005."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/173668.168635"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629175.1629203"}],"event":{"name":"ESWeek '11: Seventh Embedded Systems Week","location":"Taipei Taiwan","acronym":"ESWeek '11","sponsor":["CEDA","SIGBED ACM Special Interest Group on Embedded Systems","SIGDA ACM Special Interest Group on Design Automation","IEEE CAS","SIGMICRO ACM Special Interest Group on Microarchitectural Research and Processing","IEEE CS"]},"container-title":["Proceedings of the ninth ACM international conference on Embedded software"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2038642.2038687","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2038642.2038687","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:48:15Z","timestamp":1750240095000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2038642.2038687"}},"subtitle":["fully verified software fault isolation"],"short-title":[],"issued":{"date-parts":[[2011,10,9]]},"references-count":25,"alternative-id":["10.1145\/2038642.2038687","10.1145\/2038642"],"URL":"https:\/\/doi.org\/10.1145\/2038642.2038687","relation":{},"subject":[],"published":{"date-parts":[[2011,10,9]]},"assertion":[{"value":"2011-10-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}