{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:41:19Z","timestamp":1780994479850,"version":"3.54.1"},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2016,5,10]],"date-time":"2016-05-10T00:00:00Z","timestamp":1462838400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"NWO","award":["612.001.014"],"award-info":[{"award-number":["612.001.014"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2016,12]]},"DOI":"10.1007\/s10817-016-9369-1","type":"journal-article","created":{"date-parts":[[2016,5,10]],"date-time":"2016-05-10T02:07:49Z","timestamp":1462846069000},"page":"319-387","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["A Formal C Memory Model for Separation Logic"],"prefix":"10.1007","volume":"57","author":[{"given":"Robbert","family":"Krebbers","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,5,10]]},"reference":[{"key":"9369_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":"9369_CR2","unstructured":"Affeldt, R., Sakaguchi, K.: An intrinsic encoding of a subset of C and its application to TLS network packet processing. JFR. 7(1), 63\u2013104 (2014)"},{"key":"9369_CR3","volume-title":"Program Logics for Certified Compilers","year":"2014","unstructured":"Appel, A.W. (ed.): Program Logics for Certified Compilers. Cambridge University Press, Cambridge (2014)"},{"key":"9369_CR4","doi-asserted-by":"crossref","unstructured":"Batty, M., Memarian, K., Nienhuis, K. Pichon-Pharabod, J., Sewell, P.: The problem of programming language concurrency semantics. In: ESOP, volume 9032 of LNCS, pp. 283\u2013307 (2015)","DOI":"10.1007\/978-3-662-46669-8_12"},{"key":"9369_CR5","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\/1926385.1926394"},{"key":"9369_CR6","doi-asserted-by":"crossref","unstructured":"Bengtson, J., Jensen, J.B., Sieczkowski, F., Birkedal, L.: Verifying Object-oriented programs with higher-order separation logic in Coq. In: ITP, volume 6898 of LNCS, pp. 22\u201338 (2011)","DOI":"10.1007\/978-3-642-22863-6_5"},{"key":"9369_CR7","doi-asserted-by":"crossref","unstructured":"Beringer, L., Stewart, G., Dockins, R., Appel, A.W.: Verified compilation for shared-memory C. In: ESOP, volume 8410 of LNCS, pp. 107\u2013127 (2014)","DOI":"10.1007\/978-3-642-54833-8_7"},{"key":"9369_CR8","doi-asserted-by":"crossref","unstructured":"Besson, F., Blazy, S., Wilke, P.: A precise and abstract memory model for C using symbolic values. In: APLAS, volume 8858 of LNCS, pp. 449\u2013468 (2014)","DOI":"10.1007\/978-3-319-12736-1_24"},{"key":"9369_CR9","doi-asserted-by":"crossref","unstructured":"Boldo, S., Jourdan, J.-H., Leroy, X., Melquiond, G.: A formally-verified C compiler supporting floating-point arithmetic. In: ARITH, pp. 107\u2013115 (2013)","DOI":"10.1109\/ARITH.2013.30"},{"key":"9369_CR10","doi-asserted-by":"crossref","unstructured":"Boldo, S., Melquiond, G.: Flocq: a unified library for proving floating-point algorithms in Coq. In: ARITH, pp. 243\u2013252 (2011)","DOI":"10.1109\/ARITH.2011.40"},{"key":"9369_CR11","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: POPL, pp. 259\u2013270 (2005)","DOI":"10.1145\/1040305.1040327"},{"key":"9369_CR12","doi-asserted-by":"crossref","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: SAS, volume 2694 of LNCS, pp. 55\u201372 (2003)","DOI":"10.1007\/3-540-44898-5_4"},{"key":"9369_CR13","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: LICS, pp. 366\u2013378 (2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"9369_CR14","first-page":"85","volume":"254","author":"E Cohen","year":"2009","unstructured":"Cohen, E., Moskal, M., Tobies, S., Schulte, W.: A precise yet efficient memory model for C. ENTCS 254, 85\u2013103 (2009)","journal-title":"ENTCS"},{"key":"9369_CR15","unstructured":"Coq Development Team: The Coq proof assistant reference manual. Available at https:\/\/coq.inria.fr\/doc\/ (2015)"},{"key":"9369_CR16","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W.: Cooperating sequential processes. In: Genuys, F. (ed.) Programming Languages: NATO Advanced Study Institute, pp. 43\u2013112. Academic Press, Cambridge (1968)","DOI":"10.1007\/978-1-4757-3472-0_2"},{"key":"9369_CR17","doi-asserted-by":"crossref","unstructured":"Dockins, R., Hobor, A., Appel, A.W.: A fresh look at separation algebras and share accounting. In: APLAS, volume 5904 of LNCS, pp. 161\u2013177 (2009)","DOI":"10.1007\/978-3-642-10672-9_13"},{"key":"9369_CR18","doi-asserted-by":"crossref","unstructured":"Ellison, C.: A Formal Semantics of C with Applications. PhD thesis, University of Illinois (2012)","DOI":"10.1145\/2103621.2103719"},{"key":"9369_CR19","doi-asserted-by":"crossref","unstructured":"Ellison, C., Ro\u015fu, G.: An executable formal semantics of C with applications. In: POPL, pp. 533\u2013544 (2012)","DOI":"10.1145\/2103656.2103719"},{"key":"9369_CR20","unstructured":"GCC: The GNU Compiler Collection. Website, available at http:\/\/gcc.gnu.org\/"},{"key":"9369_CR21","doi-asserted-by":"crossref","unstructured":"Greenaway, D., Lim, J., Andronick, J., Klein, G.: Don\u2019t sweat the small stuff: formal verification of C code without the pain. In: PLDI, pp. 429\u2013439 (2014)","DOI":"10.1145\/2666356.2594296"},{"key":"9369_CR22","doi-asserted-by":"crossref","unstructured":"Hathhorn, C., Ellison, C., Ro\u015fu, G.: Defining the undefinedness of C. In: PLDI, pp. 336\u2013345 (2015)","DOI":"10.1145\/2737924.2737979"},{"key":"9369_CR23","unstructured":"Hobor, A.: Oracle Semantics. PhD thesis, Princeton University, (2008)"},{"key":"9369_CR24","doi-asserted-by":"crossref","unstructured":"Hobor, A., Appel, A.W., Nardelli, F.Z.: Oracle semantics for concurrent separation logic. In: ESOP, volume 4960 of LNCS, pp. 353\u2013367 (2008)","DOI":"10.1007\/978-3-540-78739-6_27"},{"key":"9369_CR25","unstructured":"IEEE Computer Society: 754-2008: IEEE Standard for Floating Point Arithmetic. IEEE (2008)"},{"key":"9369_CR26","unstructured":"ISO: WG14 Defect Report Summary. Website, available at http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/"},{"key":"9369_CR27","unstructured":"ISO: ISO\/IEC 9899-2011: Programming languages\u2014C. ISO Working Group 14 (2012)"},{"key":"9369_CR28","doi-asserted-by":"crossref","unstructured":"Kang, J., Hur, C.-K., Mansky, W., Garbuzov, D., Zdancewic, S., Vafeiadis, V.: A formal c memory model supporting integer-pointer casts. In: PLDI, pp. 326\u2013335 (2015)","DOI":"10.1145\/2737924.2738005"},{"key":"9369_CR29","doi-asserted-by":"crossref","unstructured":"Klein, G., Kolanski, R., Boyton, A.: Mechanised separation algebra. In: ITP, volume 7406 of LNCS, pp. 332\u2013337 (2012)","DOI":"10.1007\/978-3-642-32347-8_22"},{"key":"9369_CR30","doi-asserted-by":"crossref","unstructured":"Krebbers, R.: Aliasing restrictions of C11 formalized in Coq. In: CPP, volume 8307 of LNCS (2013)","DOI":"10.1007\/978-3-319-03545-1_4"},{"key":"9369_CR31","doi-asserted-by":"crossref","unstructured":"Krebbers, R.: An operational and axiomatic semantics for non-determinism and sequence points in C. In: POPL, pp. 101\u2013112 (2014)","DOI":"10.1145\/2535838.2535878"},{"key":"9369_CR32","doi-asserted-by":"crossref","unstructured":"Krebbers, R.: Separation algebras for C verification in Coq. In: VSTTE, volume 8471 of LNCS, pp. 150\u2013166 (2014)","DOI":"10.1007\/978-3-319-12154-3_10"},{"key":"9369_CR33","unstructured":"Krebbers, R.: The C standard formalized in Coq. PhD thesis, Radboud University (2015)"},{"key":"9369_CR34","doi-asserted-by":"crossref","unstructured":"Krebbers, R., Leroy, X., Wiedijk, F.: Formal C semantics: CompCert and the C standard. In: ITP, volume 8558 of LNCS, pp. 543\u2013548 (2014)","DOI":"10.1007\/978-3-319-08970-6_36"},{"key":"9369_CR35","doi-asserted-by":"crossref","unstructured":"Krebbers, R., Wiedijk, F.: A formalization of the C99 standard in HOL, Isabelle and Coq. In: CICM, volume 6824 of LNCS, pp. 297\u2013299 (2011)","DOI":"10.1007\/978-3-642-22673-1_28"},{"key":"9369_CR36","doi-asserted-by":"crossref","unstructured":"Krebbers, R., Wiedijk, F.: Separation logic for non-local control flow and block scope variables. In: FoSSaCS, volume 7794 of LNCS, pp. 257\u2013272 (2013)","DOI":"10.1007\/978-3-642-37075-5_17"},{"key":"9369_CR37","doi-asserted-by":"crossref","unstructured":"Krebbers, R., Wiedijk, F.: A typed C11 semantics for interactive theorem proving. In: CPP, pp. 15\u201327 (2015)","DOI":"10.1145\/2676724.2693571"},{"key":"9369_CR38","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: POPL, pp. 42\u201354 (2006)","DOI":"10.1145\/1111037.1111042"},{"issue":"7","key":"9369_CR39","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. CACM 52(7), 107\u2013115 (2009)","journal-title":"CACM"},{"key":"9369_CR40","unstructured":"Leroy, X., Appel, A.W., Blazy, S., Stewart, G.: The CompCert Memory Model, Version 2. Research report RR-7987, INRIA. Revised version available as Chapter 32 of\u00a0[3] (2012)"},{"issue":"1","key":"9369_CR41","doi-asserted-by":"crossref","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 41(1), 1\u201331 (2008)","journal-title":"JAR"},{"key":"9369_CR42","unstructured":"Maclaren, N.: What is an Object in C Terms? Mailing list message. Available at http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/9350 (2001)"},{"key":"9369_CR43","doi-asserted-by":"crossref","unstructured":"Monin, J., Shi, X.: Handcrafted Inversions made operational on operational semantics. In: ITP, volume 7998 of LNCS, pp. 338\u2013353 (2013)","DOI":"10.1007\/978-3-642-39634-2_25"},{"key":"9369_CR44","unstructured":"Norrish, M.: C formalised in HOL. PhD thesis, University of Cambridge (1998)"},{"key":"9369_CR45","doi-asserted-by":"crossref","unstructured":"Norrish, M.: Deterministic expressions in C. In: ESOP, volume 1576 of LNCS, pp. 147\u2013161 (1999)","DOI":"10.1007\/3-540-49099-X_10"},{"key":"9369_CR46","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. In: CONCUR, volume 3170 of LNCS, pp. 49\u201367 (2004)","DOI":"10.1007\/978-3-540-28644-8_4"},{"key":"9369_CR47","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang., H.: Local reasoning about programs that alter data structures. In: CSL, volume 2142 of LNCS, pp. 1\u201319 (2001)","DOI":"10.1007\/3-540-44802-0_1"},{"key":"9369_CR48","doi-asserted-by":"crossref","unstructured":"Ramananandro, T., Dos\u00a0Reis, G., Leroy, X.: Formal verification of object layout for C++ multiple inheritance. In: POPL, pp. 67\u201380 (2011)","DOI":"10.1145\/1926385.1926395"},{"key":"9369_CR49","doi-asserted-by":"crossref","unstructured":"Regehr, J., Chen, Y., Cuoq, P., Eide, E., Ellison, C., Yang, X.: Test-case reduction for C compiler bugs. In: PLDI, pp. 335\u2013346 (2012)","DOI":"10.1145\/2254064.2254104"},{"key":"9369_CR50","doi-asserted-by":"crossref","unstructured":"Robert, V., Leroy, X.: A formally-verified alias analysis. In: CPP, volume 7679 of LNCS, pp. 11\u201326 (2012)","DOI":"10.1007\/978-3-642-35308-6_5"},{"key":"9369_CR51","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\/217838.217860"},{"issue":"3","key":"9369_CR52","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1145\/2487241.2487248","volume":"60","author":"J Sevc\u00edk","year":"2013","unstructured":"Sevc\u00edk, J., Vafeiadis, V., Nardelli, F.Z., Jagannathan, S., Sewell, P.: CompCertTSO: a verified compiler for relaxed-memory concurrency. JACM 60(3), 22 (2013)","journal-title":"JACM"},{"issue":"7","key":"9369_CR53","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1145\/1785414.1785443","volume":"53","author":"P Sewell","year":"2010","unstructured":"Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-TSO: a rigorous and usable programmer\u2019s model for x86 multiprocessors. CACM 53(7), 89\u201397 (2010)","journal-title":"CACM"},{"key":"9369_CR54","unstructured":"Sozeau, M.: A new look at generalized rewriting in type theory. JFR. 2(1), 41\u201362 (2009)"},{"issue":"4","key":"9369_CR55","doi-asserted-by":"crossref","first-page":"795","DOI":"10.1017\/S0960129511000119","volume":"21","author":"B Spitters","year":"2011","unstructured":"Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. Math. Struct. Comput. Sci. 21(4), 795\u2013825 (2011)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9369_CR56","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\/1190216.1190234"},{"key":"9369_CR57","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Balabonski, T., Chakraborty, S., Morisset, R., Nardelli, F.Z.: Common compiler optimisations are invalid in the C11 memory model and what we can do about it. In: POPL, pp. 209\u2013220 (2015)","DOI":"10.1145\/2676726.2676995"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9369-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-016-9369-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9369-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9369-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,7]],"date-time":"2019-09-07T09:14:39Z","timestamp":1567847679000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9369-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,5,10]]},"references-count":57,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,12]]}},"alternative-id":["9369"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9369-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,5,10]]}}}