{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T02:43:59Z","timestamp":1725763439816},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319035444"},{"type":"electronic","value":"9783319035451"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-319-03545-1_14","type":"book-chapter","created":{"date-parts":[[2013,12,9]],"date-time":"2013-12-09T11:31:48Z","timestamp":1386588708000},"page":"211-226","source":"Crossref","is-referenced-by-count":0,"title":["Formalizing the SAFECode Type System"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Huang","sequence":"first","affiliation":[]},{"given":"Greg","family":"Morrisett","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"Coq\u00a0Proof Assistant, \n                    \n                      http:\/\/coq.inria.fr\/"},{"key":"14_CR2","unstructured":"Carlisle, M.C.: Olden: Parallelizing Programs with Dynamic Data Structures on Distributed-Memory Machines. PhD thesis (1996)"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Castro, M., Costa, M., Martin, J.-P., Peinado, M., Akritidis, P., Donnelly, A., Barham, P., Black, R.: Fast Byte-Granularity Software Fault Isolation. In: Proc., SOSP 2009 (2009)","DOI":"10.1145\/1629575.1629581"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Criswell, J., Lenharth, A., Dhurjati, D., Adve, V.: Secure Virtual Architecture: A Safe Execution Environment for Commodity Operating Systems. In: Proc., SOSP 2007 (2007)","DOI":"10.1145\/1294261.1294295"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Dhurjati, D., Kowshik, S., Adve, V.: SAFECode: Enforcing Alias Analysis for Weakly Typed Languages. In: Proc., PLDI 2006 (2006)","DOI":"10.1145\/1133981.1133999"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Grossman, D., Morrisett, G., Jim, T., Hicks, M., Wang, Y., Cheney, J.: Region-Based Memory Management in Cyclone. In: Proc., PLDI 2002 (2002)","DOI":"10.1145\/512529.512563"},{"key":"14_CR7","unstructured":"Lattner, C., Adve, V.: LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In: Proc. International Symposium on Code Generation and Optimization, CGO 2004 (March 2004)"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM\u00a052(7) (July 2009)","DOI":"10.1145\/1538788.1538814"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Leroy, X., Blazy, S.: Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations. J. Autom. Reason.\u00a041(1) (July 2008)","DOI":"10.1007\/s10817-008-9099-0"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Nagarakatte, S., Zhao, J., Martin, M.M.K., Zdancewic, S.: SoftBound: Highly Compatible and Complete Spatial Memory Safety for C. In: Proc. PLDI 2009 (2009)","DOI":"10.1145\/1542476.1542504"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Necula, G.C., McPeak, S., Weimer, W.: CCured: Type-Safe Retrofitting of Legacy Code. In: Proc. POPL (2002)","DOI":"10.1145\/503272.503286"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Tofte, M., Talpin, J.-P.: Region-based memory management. Inf. Comput.\u00a0132(2) (February 1997)","DOI":"10.1006\/inco.1996.2613"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Zhao, J., Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Formalizing the LLVM Intermediate Representation for Verified Program Transformations. In: Proc. POPL 2012 (2012)","DOI":"10.1145\/2103656.2103709"}],"container-title":["Lecture Notes in Computer Science","Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-03545-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T05:31:52Z","timestamp":1558762312000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-03545-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783319035444","9783319035451"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-03545-1_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}