{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:20Z","timestamp":1780994540706,"version":"3.54.1"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319035444","type":"print"},{"value":"9783319035451","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"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":[[2013]]},"DOI":"10.1007\/978-3-319-03545-1_4","type":"book-chapter","created":{"date-parts":[[2013,12,9]],"date-time":"2013-12-09T16:31:48Z","timestamp":1386606708000},"page":"50-65","source":"Crossref","is-referenced-by-count":23,"title":["Aliasing Restrictions of C11 Formalized in Coq"],"prefix":"10.1007","author":[{"given":"Robbert","family":"Krebbers","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Affeldt, R., Marti, N.: Towards formal verification of TLS network packet processing written in C. In: PLPV, pp. 35\u201346 (2013)","DOI":"10.1145\/2428116.2428124"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: POPL, pp. 55\u201366 (2011)","DOI":"10.1145\/1925844.1926394"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: POPL, pp. 533\u2013544 (2012)","DOI":"10.1145\/2103621.2103719"},{"key":"4_CR4","unstructured":"GNU. GCC, the GNU Compiler Collection (2011), \n                      http:\/\/gcc.gnu.org\/"},{"key":"4_CR5","unstructured":"International Organization for Standardization. WG14 Defect Report Summary (2008), \n                      http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/"},{"key":"4_CR6","unstructured":"International Organization for Standardization. ISO\/IEC 9899-2011: Programming languages \u2013 C. ISO Working Group 14 (2012)"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Krebbers, R.: An operational and axiomatic semantics for non-determinism and sequence points in C. To appear in: POPL 2014 (2013)","DOI":"10.1145\/2535838.2535878"},{"key":"4_CR8","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-642-22673-1_28","volume-title":"Intelligent Computer Mathematics","author":"R. Krebbers","year":"2011","unstructured":"Krebbers, R., Wiedijk, F.: A Formalization of the C99 Standard in HOL, Isabelle and Coq. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus\/MKM 2011. LNCS (LNAI), vol.\u00a06824, pp. 301\u2013303. Springer, Heidelberg (2011)"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/978-3-642-37075-5_17","volume-title":"Foundations of Software Science and Computation Structures","author":"R. Krebbers","year":"2013","unstructured":"Krebbers, R., Wiedijk, F.: Separation Logic for Non-local Control Flow and Block Scope Variables. In: Pfenning, F. (ed.) FOSSACS 2013. LNCS, vol.\u00a07794, pp. 257\u2013272. Springer, Heidelberg (2013)"},{"key":"4_CR10","unstructured":"Leroy, X., Appel, A.W., Blazy, S., Stewart, G.: The CompCert Memory Model, Version 2. Research report RR-7987, INRIA (2012)"},{"issue":"1","key":"4_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-008-9099-0","volume":"41","author":"X. Leroy","year":"2008","unstructured":"Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program transformations. JAR\u00a041(1), 1\u201331 (2008)","journal-title":"JAR"},{"key":"4_CR12","unstructured":"Maclaren, N.: What is an Object in C Terms?, Mailing list message (2001), \n                      http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/9350"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Nita, M., Grossman, D., Chambers, C.: A theory of platform-dependent low-level software. In: POPL, pp. 209\u2013220 (2008)","DOI":"10.1145\/1328897.1328465"},{"key":"4_CR14","unstructured":"Norrish, M.: C formalised in HOL. PhD thesis, University of Cambridge (1998)"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Ramananandro, T., Dos Reis, G., Leroy, X.: Formal verification of object layout for C++ multiple inheritance. In: POPL, pp. 67\u201380 (2011)","DOI":"10.1145\/1925844.1926395"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/978-3-642-35308-6_5","volume-title":"Certified Programs and Proofs","author":"V. Robert","year":"2012","unstructured":"Robert, V., Leroy, X.: A Formally-Verified Alias Analysis. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol.\u00a07679, pp. 11\u201326. Springer, Heidelberg (2012)"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Rossie, J.G., Friedman, D.P.: An Algebraic Semantics of Subobjects. In: OOPSLA, pp. 187\u2013199 (1995)","DOI":"10.1145\/217839.217860"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: POPL, pp. 97\u2013108 (2007)","DOI":"10.1145\/1190215.1190234"}],"container-title":["Lecture Notes in Computer Science","Certified Programs and Proofs"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-03545-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,30]],"date-time":"2023-01-30T22:32:54Z","timestamp":1675117974000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-03545-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783319035444","9783319035451"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-03545-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}