{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T16:02:25Z","timestamp":1781798545077,"version":"3.54.5"},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2018,11,16]],"date-time":"2018-11-16T00:00:00Z","timestamp":1542326400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2018,11,16]],"date-time":"2018-11-16T00:00:00Z","timestamp":1542326400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1521523"],"award-info":[{"award-number":["1521523"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"crossref","award":["ANR-14-CE28-0014"],"award-info":[{"award-number":["ANR-14-CE28-0014"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-12-2-0293"],"award-info":[{"award-number":["FA8750-12-2-0293"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2019,8]]},"DOI":"10.1007\/s10817-018-9496-y","type":"journal-article","created":{"date-parts":[[2018,11,16]],"date-time":"2018-11-16T11:40:13Z","timestamp":1542368413000},"page":"369-392","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["CompCertS: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics"],"prefix":"10.1007","volume":"63","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Besson","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"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":[[2018,11,16]]},"reference":[{"key":"9496_CR1","unstructured":"Bedin Franca, R., Blazy, S., Favre-Felix, D., Leroy, X., Pantel, M., Souyris, J.: Formally verified optimizing compilation in ACG-based flight control software. In: ERTS 2012: Embedded Real Time Software and Systems (2012)"},{"key":"9496_CR2","unstructured":"Besson, F., Blazy, S., Wilke, P.: Companion website. \n                    http:\/\/www.cs.yale.edu\/homes\/wilke-pierre\/jar18\/"},{"key":"9496_CR3","doi-asserted-by":"crossref","unstructured":"Besson, F., Blazy, S., Wilke, P.: A precise and abstract memory model for C using symbolic values. In: APLAS, LNCS, vol. 8858 (2014)","DOI":"10.1007\/978-3-319-12736-1_24"},{"key":"9496_CR4","doi-asserted-by":"crossref","unstructured":"Besson, F., Blazy, S., Wilke, P.: A concrete memory model for CompCert. In: ITP, LNCS, vol. 9236. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-22102-1_5"},{"key":"9496_CR5","doi-asserted-by":"publisher","unstructured":"Besson, F., Blazy, S., Wilke, P.: A Verified CompCert Front-End for a Memory Model supporting Pointer Arithmetic and Uninitialised Data. Journal of Automated Reasoning pp. 1\u201348 (2017). \n                    https:\/\/doi.org\/10.1007\/s10817-017-9439-z","DOI":"10.1007\/s10817-017-9439-z"},{"key":"9496_CR6","doi-asserted-by":"crossref","unstructured":"Blazy, S., Trieu, A.: Formal verification of control-flow graph flattening. In: CPP. ACM, New York (2016)","DOI":"10.1145\/2854065.2854082"},{"key":"9496_CR7","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. ACM, New York (2014)","DOI":"10.1145\/2594291.2594301"},{"key":"9496_CR8","doi-asserted-by":"publisher","unstructured":"Ellison, C., Rosu, G.: An executable formal semantics of C with applications. SIGPLAN Not. 47(1) (2012). \n                    https:\/\/doi.org\/10.1145\/2103621.2103719","DOI":"10.1145\/2103621.2103719"},{"key":"9496_CR9","doi-asserted-by":"crossref","unstructured":"Hathhorn, C., Ellison, C., Rosu, G.: Defining the undefinedness of C. In: PLDI. ACM, New York (2015)","DOI":"10.1145\/2737924.2737979"},{"key":"9496_CR10","unstructured":"ISO: ISO C Standard 2011. Tech. rep. (2011)"},{"key":"9496_CR11","doi-asserted-by":"crossref","unstructured":"Kang, J., Hur, C., Mansky, W., Garbuzov, D., Zdancewic, S., Vafeiadis, V.: A formal C memory model supporting integer-pointer casts. In: PLDI (2015)","DOI":"10.1145\/2737924.2738005"},{"key":"9496_CR12","doi-asserted-by":"publisher","unstructured":"Krebbers, R.: Aliasing restrictions of C11 formalized in Coq. In: CPP, LNCS, vol. 8307. Springer, Berlin (2013). \n                    https:\/\/doi.org\/10.1007\/978-3-319-03545-1_4","DOI":"10.1007\/978-3-319-03545-1_4"},{"key":"9496_CR13","doi-asserted-by":"crossref","unstructured":"Krebbers, R.: An operational and axiomatic semantics for non-determinism and sequence points in C. In: POPL. ACM, New York (2014)","DOI":"10.1145\/2535838.2535878"},{"key":"9496_CR14","unstructured":"Leroy, X.: Formal verification of a realistic compiler. C. ACM 52(7), 107\u2013115 (2009). \n                    http:\/\/gallium.inria.fr\/~xleroy\/publi\/compcert-CACM.pdf"},{"issue":"1","key":"9496_CR15","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":"9496_CR16","doi-asserted-by":"crossref","unstructured":"Memarian, K., Matthiesen, J., Lingard, J., Nienhuis, K., Chisnall, D., Watson, R.N., Sewell, P.: Into the depths of C: elaborating the de facto standards. In: PLDI. ACM, New York (2016)","DOI":"10.1145\/2908080.2908081"},{"key":"9496_CR17","doi-asserted-by":"publisher","unstructured":"Mullen, E., Zuniga, D., Tatlock, Z., Grossman, D.: Verified peephole optimizations for CompCert. In: PLDI, pp. 448\u2013461. ACM, New York (2016). \n                    https:\/\/doi.org\/10.1145\/2908080","DOI":"10.1145\/2908080"},{"key":"9496_CR18","unstructured":"Norrish, M.: C formalised in hol. Ph.D. thesis, University of Cambridge, Cambridge (1998)"},{"key":"9496_CR19","unstructured":"Robert, V., Leroy, X.: A formally-verified alias analysis. In: CPP, LNCS, vol. 7679. Springer, Berlin (2012). \n                    http:\/\/gallium.inria.fr\/~xleroy\/publi\/alias-analysis.pdf"},{"issue":"3","key":"9496_CR20","doi-asserted-by":"publisher","first-page":"22:1","DOI":"10.1145\/2487241.2487248","volume":"60","author":"J \u0160ev\u010d\u00edk","year":"2013","unstructured":"\u0160ev\u010d\u00edk, J., Vafeiadis, V., Zappa\u00a0Nardelli, F., Jagannathan, S., Sewell, P.: CompCertTSO: A verified compiler for relaxed-memory concurrency. J. ACM 60(3), 22:1\u201322:50 (2013). \n                    https:\/\/doi.org\/10.1145\/2487241.2487248","journal-title":"J. ACM"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9496-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9496-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9496-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,13]],"date-time":"2020-05-13T23:02:27Z","timestamp":1589410947000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9496-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,11,16]]},"references-count":20,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,8]]}},"alternative-id":["9496"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9496-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,11,16]]},"assertion":[{"value":"26 February 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 October 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 November 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}