{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,16]],"date-time":"2025-06-16T16:04:41Z","timestamp":1750089881846,"version":"3.40.3"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661063"},{"type":"electronic","value":"9783319661070"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66107-0_6","type":"book-chapter","created":{"date-parts":[[2017,8,20]],"date-time":"2017-08-20T14:13:59Z","timestamp":1503238439000},"page":"81-97","source":"Crossref","is-referenced-by-count":8,"title":["CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6815-0652","authenticated-orcid":false,"given":"Fr\u00e9d\u00e9ric","family":"Besson","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0189-0223","authenticated-orcid":false,"given":"Sandrine","family":"Blazy","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9681-644X","authenticated-orcid":false,"given":"Pierre","family":"Wilke","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","unstructured":"Companion website. http:\/\/www.cs.yale.edu\/homes\/wilke-pierre\/itp17\/"},{"key":"6_CR2","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":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Cham (2014). doi:10.1007\/978-3-319-12736-1_24"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-319-22102-1_5","volume-title":"Interactive Theorem Proving","author":"F Besson","year":"2015","unstructured":"Besson, F., Blazy, S., Wilke, P.: A concrete memory model for CompCert. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 67\u201383. Springer, Cham (2015). doi:10.1007\/978-3-319-22102-1_5"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Blazy, S., Trieu, A.: Formal verification of control-flow graph flattening. In: CPP. ACM (2016)","DOI":"10.1145\/2854065.2854082"},{"key":"6_CR6","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 (2014)","DOI":"10.1145\/2594291.2594301"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Hathhorn, C., Ellison, C., Rosu, G.: Defining the undefinedness of C. In: PLDI. ACM (2015)","DOI":"10.1145\/2737924.2737979"},{"key":"6_CR8","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":"6_CR9","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, Cham (2013). doi:10.1007\/978-3-319-03545-1_4"},{"key":"6_CR10","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":"6_CR11","doi-asserted-by":"crossref","unstructured":"Kroll, J.A., Stewart, G., Appel, A.W.: Portable software fault isolation. In: CSF. IEEE (2014)","DOI":"10.1109\/CSF.2014.10"},{"issue":"7","key":"6_CR12","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":"6_CR13","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 (2016)","DOI":"10.1145\/2908080.2908081"},{"key":"6_CR14","unstructured":"Norrish, M.: C formalised in HOL. Ph.D. thesis, University of Cambridge (1998)"},{"key":"6_CR15","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. 7679, pp. 11\u201326. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-35308-6_5"},{"issue":"3","key":"6_CR16","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 Nardelli, F., Jagannathan, S., Sewell, P.: CompCertTSO: a verified compiler for relaxed-memory concurrency. J. ACM 60(3), 22:1\u201322:50 (2013)","journal-title":"J. ACM"}],"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-66107-0_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,29]],"date-time":"2022-09-29T06:04:25Z","timestamp":1664431465000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-66107-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661063","9783319661070"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66107-0_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}