{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:35Z","timestamp":1780994555771,"version":"3.54.1"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2017,11,3]],"date-time":"2017-11-03T00:00:00Z","timestamp":1509667200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2019,4]]},"DOI":"10.1007\/s10817-017-9439-z","type":"journal-article","created":{"date-parts":[[2017,11,3]],"date-time":"2017-11-03T07:53:59Z","timestamp":1509695639000},"page":"433-480","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data"],"prefix":"10.1007","volume":"62","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6815-0652","authenticated-orcid":false,"given":"Fr\u00e9d\u00e9ric","family":"Besson","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0189-0223","authenticated-orcid":false,"given":"Sandrine","family":"Blazy","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9681-644X","authenticated-orcid":false,"given":"Pierre","family":"Wilke","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,11,3]]},"reference":[{"issue":"7","key":"9439_CR1","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. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"9439_CR2","doi-asserted-by":"publisher","unstructured":"Jourdan, J., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: POPL (2015). doi:\n                    10.1145\/2676726.2676966","DOI":"10.1145\/2676726.2676966"},{"key":"9439_CR3","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":"9439_CR4","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 \u201912 (2012)","DOI":"10.1145\/2349896.2349905"},{"key":"9439_CR5","unstructured":"Leroy, X., Appel, A.W., Blazy, S., Stewart, G.: The CompCert memory model. In: Program Logics for Certified Compilers. Cambridge University Press (2014). \n                    http:\/\/hal.inria.fr\/hal-00905435"},{"issue":"1","key":"9439_CR6","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. Reason. 41(1), 1\u201331 (2008)","journal-title":"J. Autom. Reason."},{"key":"9439_CR7","unstructured":"Besson, F., Blazy, S., Wilke, P.: Companion website with Coq development. \n                    http:\/\/www.irisa.fr\/celtique\/ext\/frontend-symbolic"},{"key":"9439_CR8","unstructured":"ISO: C Standard 1999. Technical report, ISO (1999). \n                    http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/n1256.pdf"},{"issue":"4","key":"9439_CR9","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43(4), 363\u2013446 (2009). doi:\n                    10.1007\/s10817-009-9155-4","journal-title":"J. Autom. Reason."},{"key":"9439_CR10","unstructured":"MIRA Ltd: MISRA-C:2004 Guidelines for the use of the C language in critical systems (2004). \n                    www.misra.org.uk"},{"key":"9439_CR11","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":"9439_CR12","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: TACAS, LNCS, vol. 4963. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9439_CR13","doi-asserted-by":"publisher","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14\u201320, 2011. Proceedings, chap. CVC4, pp. 171\u2013177. Springer, Berlin, Heidelberg (2011). \n                    10.1007\/978-3-642-22110-1_14","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"9439_CR14","unstructured":"Lee, D.: A memory allocator. \n                    http:\/\/gee.cs.oswego.edu\/dl\/html\/malloc.html"},{"key":"9439_CR15","doi-asserted-by":"crossref","unstructured":"Bernstein, D.J., Lange, T., Schwabe, P.: The Security Impact of a New Cryptographic Library. In: LATINCRYPT\u201912, LNCS, vol. 7533, pp. 159\u2013176. Springer (2012)","DOI":"10.1007\/978-3-642-33481-8_9"},{"key":"9439_CR16","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"},{"key":"9439_CR17","unstructured":"Blazy, S.: Experiments in validating formal semantics for C. In: C\/C\n                    \n                      \n                    \n                    $$++$$\n                    \n                      \n                        \n                          +\n                          +\n                        \n                      \n                    \n                   Verification Workshop. Raboud University Nijmegen report ICIS-R07015 (2007)"},{"key":"9439_CR18","unstructured":"ISO: C Standard 2011. Technical report, ISO (1999). \n                    http:\/\/www.open-std.org\/JTC1\/SC22\/WG14\/www\/docs\/n1570.pdf"},{"key":"9439_CR19","unstructured":"Norrish, M.: C formalised in HOL. Ph.D. thesis, University of Cambridge (1998)"},{"key":"9439_CR20","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":"9439_CR21","doi-asserted-by":"crossref","unstructured":"Cohen, E., Moskal, M., Tobies, S., Schulte, W.: A precise yet efficient memory model for C. ENTCS 254 (2009)","DOI":"10.1016\/j.entcs.2009.09.061"},{"key":"9439_CR22","doi-asserted-by":"crossref","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M.A., Leinenbach, D., Moskal, M., al.: VCC: A practical system for verifying concurrent C. In: TPHOLs, LNCS, vol. 5674. Springer (2009)","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"9439_CR23","doi-asserted-by":"crossref","unstructured":"Greenaway, D., Andronick, J., Klein, G.: Bridging the gap: automatic verified abstraction of C. In: ITP, LNCS, vol. 7406. Springer (2012)","DOI":"10.1007\/978-3-642-32347-8_8"},{"key":"9439_CR24","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":"9439_CR25","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":"9439_CR26","doi-asserted-by":"publisher","unstructured":"Hathhorn, C., Ellison, C., Ro\u015fu, G.: Defining the undefinedness of c. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201915), pp. 336\u2013345. ACM (2015). doi:\n                    10.1145\/2813885.2737979","DOI":"10.1145\/2813885.2737979"},{"key":"9439_CR27","doi-asserted-by":"crossref","unstructured":"Blazy, S., Leroy, X.: Mechanized semantics for the clight subset of the C language. J. Autom. Reason. 43(3) (2009)","DOI":"10.1007\/s10817-009-9148-3"},{"key":"9439_CR28","unstructured":"Bedin\u00a0Fran\u00e7a, R., Blazy, S., Favre-Felix, D., Leroy, X., Pantel, M., Souyris, J.: Formally verified optimizing compilation in ACG-based flight control software. In: ERTS2 (2012). \n                    https:\/\/hal.inria.fr\/hal-00653367"},{"key":"9439_CR29","doi-asserted-by":"crossref","unstructured":"Krebbers, R., Leroy, X., Wiedijk, F.: Formal C semantics: Compcert and the C standard. In: ITP 2014, LNCS, vol. 8558. Springer (2014)","DOI":"10.1007\/978-3-319-08970-6_36"},{"key":"9439_CR30","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":"9439_CR31","doi-asserted-by":"publisher","unstructured":"Krebbers, R.: Aliasing restrictions of C11 formalized in Coq. In: CPP, LNCS, vol. 8307. Springer (2013). \ndoi:\n                    10.1007\/978-3-319-03545-1_4","DOI":"10.1007\/978-3-319-03545-1_4"},{"key":"9439_CR32","doi-asserted-by":"crossref","unstructured":"Carbonneaux, Q., Hoffmann, J., Ramananandro, T., Shao, Z.: End-to-end verification of stack-space bounds for C programs. In: PLDI\u201914, p.\u00a030. ACM (2014)","DOI":"10.1145\/2594291.2594301"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9439-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-017-9439-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9439-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,25]],"date-time":"2019-04-25T11:17:32Z","timestamp":1556191052000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-017-9439-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11,3]]},"references-count":32,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,4]]}},"alternative-id":["9439"],"URL":"https:\/\/doi.org\/10.1007\/s10817-017-9439-z","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,11,3]]},"assertion":[{"value":"3 October 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 October 2017","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 November 2017","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}