{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:05:06Z","timestamp":1770271506925,"version":"3.49.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319221014","type":"print"},{"value":"9783319221021","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-22102-1_5","type":"book-chapter","created":{"date-parts":[[2015,8,18]],"date-time":"2015-08-18T08:30:14Z","timestamp":1439886614000},"page":"67-83","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["A Concrete Memory Model for CompCert"],"prefix":"10.1007","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Besson","sequence":"first","affiliation":[]},{"given":"Sandrine","family":"Blazy","sequence":"additional","affiliation":[]},{"given":"Pierre","family":"Wilke","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,8,19]]},"reference":[{"key":"5_CR1","unstructured":"Companion website. URL: http:\/\/www.irisa.fr\/celtique\/ext\/new-mem"},{"key":"5_CR2","unstructured":"Fran\u00e7a, R.B., Blazy, S., Favre-Felix, D., Leroy, X., Pantel, M., Souyris, J.: Formally verified optimizing compilation in ACG-based flight control software. In: ERTS2 (2012)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"449","DOI":"10.1007\/978-3-319-12736-1_24","volume-title":"Programming Languages and Systems","author":"F Besson","year":"2014","unstructured":"Besson, F., Blazy, S., Wilke, P.: A precise and abstract memory model for C using symbolic values. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 449\u2013468. Springer, Heidelberg (2014)"},{"key":"5_CR4","unstructured":"Blazy, S.: Experiments in validating formal semantics for C. In: C\/C++ Verification Workshop. Raboud University Nijmegen report ICIS-R07015 (2007)"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Blazy, S., Leroy, X.: Mechanized Semantics for the Clight Subset of the C Language. J. Autom. Reasoning, 43(3), 263\u2013288 (2009)","DOI":"10.1007\/s10817-009-9148-3"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Clements, A.T., Kaashoek, M.F., Zeldovich, N., Morris, R.T., Kohler, E.: The scalable commutativity rule: designing scalable software for multicore processors. In: SOSP. ACM (2013)","DOI":"10.1145\/2517349.2522712"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"5_CR8","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":"5_CR9","doi-asserted-by":"crossref","unstructured":"Ellison, C., Ro\u015fu, G.: An executable formal semantics of C with applications. In: POPL. ACM (2012)","DOI":"10.1145\/2103656.2103719"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-32347-8_8","volume-title":"Interactive Theorem Proving","author":"D Greenaway","year":"2012","unstructured":"Greenaway, D., Andronick, J., Klein, G.: Bridging the gap: automatic verified abstraction of C. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 99\u2013115. Springer, Heidelberg (2012)"},{"key":"5_CR11","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. ACM (2014)","DOI":"10.1145\/2594291.2594296"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Jourdan, J., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: POPL (2015)","DOI":"10.1145\/2676726.2676966"},{"key":"5_CR13","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. ACM (2015)","DOI":"10.1145\/2737924.2738005"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-319-03545-1_4","volume-title":"Certified Programs and Proofs","author":"R Krebbers","year":"2013","unstructured":"Krebbers, R.: Aliasing restrictions of C11 formalized in Coq. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 50\u201365. Springer, Heidelberg (2013)"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Krebbers, R.: An operational and axiomatic semantics for non-determinism and sequence points in C. In: POPL. ACM (2014)","DOI":"10.1145\/2535838.2535878"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1007\/978-3-319-08970-6_36","volume-title":"Interactive Theorem Proving","author":"R Krebbers","year":"2014","unstructured":"Krebbers, R., Leroy, X., Wiedijk, F.: Formal C semantics: CompCert and the C standard. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 543\u2013548. Springer, Heidelberg (2014)"},{"issue":"7","key":"5_CR17","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. C. ACM 52(7), 107\u2013115 (2009)","journal-title":"C. ACM"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Leroy, X., Appel, A.W., Blazy, S., Stewart, G.: The CompCert memory model. In: Program Logics for Certified Compilers. Cambridge University Press (2014)","DOI":"10.1017\/CBO9781107256552"},{"issue":"1","key":"5_CR19","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. J. Autom. Reasoning 41(1), 1\u201331 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"5_CR20","unstructured":"Norrish, M.: C formalised in HOL. Ph.D. thesis, University of Cambridge (1998)"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: POPL. ACM (2007)","DOI":"10.1145\/1190216.1190234"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Wang, X., Chen, H., Cheung, A., Jia, Z., Zeldovich, N., Kaashoek, M.: Undefined behavior: What happened to my code? In: APSYS 2012 (2012)","DOI":"10.1145\/2349896.2349905"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: PLDI. ACM (2011)","DOI":"10.1145\/1993498.1993532"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-22102-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T06:01:44Z","timestamp":1676959304000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-22102-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319221014","9783319221021"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-22102-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"19 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}