{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:55Z","timestamp":1772164075971,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":59,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,6,2]],"date-time":"2017-06-02T00:00:00Z","timestamp":1496361600000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"AFRL","award":["FA8750-10-C-0237"],"award-info":[{"award-number":["FA8750-10-C-0237"]}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K008528, EP\/H005633"],"award-info":[{"award-number":["EP\/K008528, EP\/H005633"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["CTSRD"],"award-info":[{"award-number":["CTSRD"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,6,2]]},"DOI":"10.1145\/2908080.2908081","type":"proceedings-article","created":{"date-parts":[[2016,6,2]],"date-time":"2016-06-02T15:23:42Z","timestamp":1464881022000},"page":"1-15","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":62,"title":["Into the depths of C: elaborating the de facto standards"],"prefix":"10.1145","author":[{"given":"Kayvan","family":"Memarian","sequence":"first","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Justus","family":"Matthiesen","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"James","family":"Lingard","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Kyndylan","family":"Nienhuis","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"David","family":"Chisnall","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Robert N. M.","family":"Watson","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]}],"member":"320","published-online":{"date-parts":[[2016,6,2]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Programming Languages \u2014 C. 2011."},{"key":"e_1_3_2_1_2_1","unstructured":"ISO\/IEC 9899:2011. A non-final but recent version is available at www.open-std.org\/jtc1\/sc22\/wg14\/docs\/n1539.pdf."},{"key":"e_1_3_2_1_3_1","volume-title":"ANSI X3.159-1989","author":"Programming ANSI.","year":"1989","unstructured":"ANSI. Programming Languages \u2013 C: ANSI X3.159-1989. 1989."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_2_1_5_1","volume-title":"Programming Languages \u2014 C++","author":"Becker P.","year":"2011","unstructured":"P. Becker, editor. Programming Languages \u2014 C++. 2011. ISO\/IEC 14882:2011."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1646353.1646374"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12736-1_24"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_5"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375591"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/SCAM.2009.22"},{"key":"e_1_3_2_1_11_1","volume-title":"C memory object and value semantics: the space of de facto and ISO standards","author":"Chisnall D.","year":"2016","unstructured":"D. Chisnall, J. Matthiesen, K. Memarian, K. Nienhuis, P., and R.N.M. Watson. C memory object and value semantics: the space of de facto and ISO standards, 2016. http:\/\/www.cl.cam.ac.uk\/~pes20\/cerberus\/."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694367"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.09.061"},{"key":"e_1_3_2_1_14_1","unstructured":"J. Cook and S. Subramanian. A formal semantics for C in Nqthm. Technical Report 517D Trusted Information Systems October 1994."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855768.1855774"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1346281.1346295"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103719"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/647842.736414"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737979"},{"key":"e_1_3_2_1_20_1","unstructured":"Charles McEwen Ellison III. A Formal Semantics of C with Applications. PhD thesis University of Illinois at Urbana-Champaign 2012."},{"key":"e_1_3_2_1_21_1","volume-title":"Rv-match v0.1. https:\/\/runtimeverification.com\/match\/download\/","author":"Runtime Verification Inc.","year":"2016","unstructured":"Runtime Verification Inc. Rv-match v0.1. https:\/\/runtimeverification.com\/match\/download\/, 2016. Downloaded 2016-03-11."},{"key":"e_1_3_2_1_22_1","volume-title":"July","author":"Plc Intel","year":"2013","unstructured":"Intel Plc. Introduction to Intel memory protection extensions, July 2013."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/647057.713871"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738005"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/100511"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_4"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535878"},{"key":"e_1_3_2_1_28_1","unstructured":"R. Krebbers. The C standard formalized in Coq. PhD thesis Radboud University Nijmegen December 2015."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37075-5_17"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693571"},{"key":"e_1_3_2_1_31_1","volume-title":"INRIA","author":"Leroy X.","year":"2012","unstructured":"X. Leroy, A. W. Appel, S. Blazy, and G. Stewart. The CompCert memory model, version 2. Research report RR-7987, INRIA, June 2012."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"e_1_3_2_1_33_1","volume-title":"Cerberus","author":"Memarian K.","year":"2016","unstructured":"K. Memarian, J. Matthiesen, K. Nienhuis, V. B. F. Gomes, J. Lingard, D. Chisnall, R. N. M. Watson, and P. Sewell. Cerberus, 2016."},{"key":"e_1_3_2_1_34_1","unstructured":"www.cl.cam.ac.uk\/~pes20\/cerberus www.repository.cam.ac.uk\/handle\/1810\/255730."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628143"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542504"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503286"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250746"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2983997"},{"key":"e_1_3_2_1_40_1","unstructured":"M. Norrish. C formalised in HOL. Technical Report UCAMCL-TR-453 U. Cambridge Computer Laboratory 1998."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/645393.651894"},{"key":"e_1_3_2_1_42_1","unstructured":"N. S Papaspyrou. A formal semantics for the C programming language. PhD thesis National Technical University of Athens 1998."},{"key":"e_1_3_2_1_43_1","unstructured":"F. Pottier and Y. R\u00e9gis-Gianas. Menhir. gallium.inria.fr\/~fpottier\/menhir\/."},{"key":"e_1_3_2_1_44_1","unstructured":"J. Regehr. blog.regehr.org\/archives\/721 2012."},{"key":"e_1_3_2_1_45_1","unstructured":"J. Regehr April 2015. blog.regehr.org\/archives\/1234."},{"key":"e_1_3_2_1_46_1","volume-title":"trust-in-soft.com\/tis-interpreter","year":"2015","unstructured":"TrustInSoft. trust-in-soft.com\/tis-interpreter, 2015."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190234"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2349896.2349905"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522728"},{"key":"e_1_3_2_1_51_1","unstructured":"R. N. M. Watson P. G. Neumann J. Woodruff M. Roe J. Anderson D. Chisnall B. Davis A. Joannou B. Laurie S. W. Moore S. J. Murdoch and R. Norton. Capability hardware enhanced RISC instructions: CHERI instruction-set architecture. Technical Report UCAM-CL-TR-864 University of Cambridge Computer Laboratory November 2015."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.9"},{"key":"e_1_3_2_1_53_1","unstructured":"WG14. Defect report summary for ISO\/IEC 9899:1999."},{"key":"e_1_3_2_1_54_1","unstructured":"WG14. ISO\/IEC 9899:2011."},{"key":"e_1_3_2_1_55_1","volume-title":"Defect report","year":"2004","unstructured":"WG14. Defect report 260, September 2004."},{"key":"e_1_3_2_1_56_1","unstructured":"www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/dr_260.htm."},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.5555\/2665671.2665740"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103709"}],"event":{"name":"PLDI '16: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Santa Barbara CA USA","acronym":"PLDI '16","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2908080.2908081","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2908080.2908081","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2908080.2908081","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:20:58Z","timestamp":1763457658000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2908080.2908081"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,2]]},"references-count":59,"alternative-id":["10.1145\/2908080.2908081","10.1145\/2908080"],"URL":"https:\/\/doi.org\/10.1145\/2908080.2908081","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2980983.2908081","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2016,6,2]]},"assertion":[{"value":"2016-06-02","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}