{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T23:11:07Z","timestamp":1765667467662,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572586"},{"type":"electronic","value":"9783031572593"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,6]],"date-time":"2024-04-06T00:00:00Z","timestamp":1712361600000},"content-version":"vor","delay-in-days":96,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>CompCert is a formally verified compiler for C that is specified, programmed and proved correct with the Coq proof assistant. CompCert was used in industry to compile critical embedded software. Its correctness proof states that the compiler does not introduce bugs. This semantic preservation property involves the formal semantics of the source and target languages of the compiler.<\/jats:p><jats:p>Reasoning on C semantics to prove compiler correctness is challenging, as C is a real language that was not designed with semantics in mind. This paper presents the operational style that was designed for the C semantics of CompCert in order to facilitate the mechanized reasoning on terminating and diverging programs, and details the semantics of the Clight source language of CompCert.\n<\/jats:p>","DOI":"10.1007\/978-3-031-57259-3_1","type":"book-chapter","created":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T13:01:39Z","timestamp":1712322099000},"page":"1-21","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["From Mechanized Semantics to Verified Compilation: the Clight Semantics of CompCert"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0189-0223","authenticated-orcid":false,"given":"Sandrine","family":"Blazy","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,6]]},"reference":[{"key":"1_CR1","unstructured":"Agda version 2.6.4 (2023), https:\/\/wiki.portal.chalmers.se\/agda\/Main\/HomePage"},{"key":"1_CR2","unstructured":"Isabelle2023 (2023), https:\/\/isabelle.in.tum.de\/"},{"key":"1_CR3","unstructured":"Online Coq development for CompCert version 3.13 (2023), https:\/\/compcert.org\/doc\/index.html"},{"key":"1_CR4","doi-asserted-by":"publisher","unstructured":"Appel, A.W., Blazy, S.: Separation logic for small-step cminor. In: Schneider, K., Brandt, J. (eds.) Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings. Lecture Notes in Computer Science, vol.\u00a04732, pp. 5\u201321. Springer (2007), https:\/\/doi.org\/10.1007\/978-3-540-74591-4_3","DOI":"10.1007\/978-3-540-74591-4_3"},{"key":"1_CR5","doi-asserted-by":"publisher","unstructured":"Barri\u00e8re, A., Blazy, S., Fl\u00fcckiger, O., Pichardie, D., Vitek, J.: Formally verified speculation and deoptimization in a JIT compiler. Proc. ACM Program. Lang. (POPL) (2021), https:\/\/doi.org\/10.1145\/3434327","DOI":"10.1145\/3434327"},{"key":"1_CR6","doi-asserted-by":"publisher","unstructured":"Barri\u00e8re, A., Blazy, S., Pichardie, D.: Formally verified native code generation in an effectful JIT: turning the CompCert backend into a formally verified JIT compiler. Proc. ACM Program. Lang. 7(POPL), 249\u2013277 (2023), https:\/\/doi.org\/10.1145\/3571202","DOI":"10.1145\/3571202"},{"key":"1_CR7","doi-asserted-by":"publisher","unstructured":"Barthe, G., Blazy, S., Gr\u00e9goire, B., Hutin, R., Laporte, V., Pichardie, D., Trieu, A.: Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. 4(POPL), 7:1\u20137:30 (2020). https:\/\/doi.org\/10.1145\/3371075, https:\/\/doi.org\/10.1145\/3371075","DOI":"10.1145\/3371075"},{"key":"1_CR8","doi-asserted-by":"publisher","unstructured":"Blazy, S., Hutin, R.: Formal verification of a program obfuscation based on mixed boolean-arithmetic expressions. In: Mahboubi, A., Myreen, M.O. (eds.) Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019. pp. 196\u2013208. ACM (2019). https:\/\/doi.org\/10.1145\/3293880.3294103, https:\/\/doi.org\/10.1145\/3293880.3294103","DOI":"10.1145\/3293880.3294103"},{"key":"1_CR9","doi-asserted-by":"publisher","unstructured":"Blazy, S., Leroy, X.: Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning 43(3), 263\u2013288 (2009). https:\/\/doi.org\/10.1007\/s10817-009-9148-3, https:\/\/hal.inria.fr\/inria-00352524","DOI":"10.1007\/s10817-009-9148-3"},{"key":"1_CR10","doi-asserted-by":"publisher","unstructured":"Bodin, M., Chargu\u00e9raud, A., Filaretti, D., Gardner, P., Maffeis, S., Naudziuniene, D., Schmitt, A., Smith, G.: A trusted mechanised javascript specification. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201914, San Diego, CA, USA, January 20-21, 2014. pp. 87\u2013100. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535876, https:\/\/doi.org\/10.1145\/2535838.2535876","DOI":"10.1145\/2535838.2535876"},{"key":"1_CR11","doi-asserted-by":"publisher","unstructured":"Bourke, T., Brun, L., Dagand, P., Leroy, X., Pouzet, M., Rieg, L.: A formally verified compiler for lustre. In: Cohen, A., Vechev, M.T. (eds.) Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017. pp. 586\u2013601. ACM (2017). https:\/\/doi.org\/10.1145\/3062341.3062358, https:\/\/doi.org\/10.1145\/3062341.3062358","DOI":"10.1145\/3062341.3062358"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Boyer, R.S., Moore, J.S.: MJRTY: A fast majority vote algorithm. In: Boyer, R.S. (ed.) Automated Reasoning: Essays in Honor of Woody Bledsoe. pp. 105\u2013118. Kluwer Academic Publishers (1991)","DOI":"10.1007\/978-94-011-3488-0_5"},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Cao, Q., Beringer, L., Gruetter, S., Dodds, J., Appel, A.W.: VST-Floyd: A separation logic tool to verify correctness of C programs. J. Autom. Reason. 61(1-4), 367\u2013422 (2018). https:\/\/doi.org\/10.1007\/S10817-018-9457-5, https:\/\/doi.org\/10.1007\/s10817-018-9457-5","DOI":"10.1007\/S10817-018-9457-5"},{"key":"1_CR14","unstructured":"Duff, T.: (1983), www.lysator.liu.se\/c\/duffs-device.html"},{"key":"1_CR15","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, J.C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Proceedings of the 22nd European Symposium on Programming. LNCS, vol.\u00a07792, pp. 125\u2013128. Springer (Mar 2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8, https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"1_CR16","doi-asserted-by":"publisher","unstructured":"Herklotz, Y., Pollard, J.D., Ramanathan, N., Wickerson, J.: Formal verification of high-level synthesis. Proc. ACM Program. Lang. 5(OOPSLA) (oct 2021). https:\/\/doi.org\/10.1145\/3485494, https:\/\/doi.org\/10.1145\/3485494","DOI":"10.1145\/3485494"},{"key":"1_CR17","unstructured":"Inria: The Coq proof assistant reference manual (2022), http:\/\/coq.inria.fr, version 8.12.1"},{"key":"1_CR18","doi-asserted-by":"publisher","unstructured":"Jourdan, J., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015. pp. 247\u2013259. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2676966, https:\/\/doi.org\/10.1145\/2676726.2676966","DOI":"10.1145\/2676726.2676966"},{"key":"1_CR19","unstructured":"K\u00e4stner, D., Barrho, J., W\u00fcnsche, U., Schlickling, M., Schommer, B., Schmidt, M., Ferdinand, C., Leroy, X., Blazy, S.: CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler. In: ERTS2 2018 - 9th European Congress Embedded Real-Time Software and Systems. pp.\u00a01\u20139. 3AF, SEE, SIE (Jan 2018)"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a java-like language, virtual machine, and compiler. ACM Trans. Program. Lang. Syst. 28(4), 619\u2013695 (jul 2006). https:\/\/doi.org\/10.1145\/1146809.1146811, https:\/\/doi.org\/10.1145\/1146809.1146811","DOI":"10.1145\/1146809.1146811"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"Koenig, J., Shao, Z.: CompCertO: Compiling certified open c components. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. p. 1095\u20131109. PLDI 2021, Association for Computing Machinery, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3453483.3454097, https:\/\/doi.org\/10.1145\/3453483.3454097","DOI":"10.1145\/3453483.3454097"},{"key":"1_CR22","unstructured":"Leino, R.M.: Program Proofs. The MIT Press (2023), https:\/\/mitpress.mit.edu\/9780262546232\/program-proofs\/"},{"key":"1_CR23","doi-asserted-by":"publisher","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM (2009). https:\/\/doi.org\/10.1145\/1538788.1538814","DOI":"10.1145\/1538788.1538814"},{"key":"1_CR24","doi-asserted-by":"publisher","unstructured":"Leroy, X.: A formally verified compiler back-end. Journal of Automated Reasoning 43(4), 363\u2013446 (2009). https:\/\/doi.org\/10.1007\/s10817-009-9155-4","DOI":"10.1007\/s10817-009-9155-4"},{"key":"1_CR25","unstructured":"Leroy, X.: Coq development for the course \"mechanized semantics\" (2019), https:\/\/github.com\/xavierleroy\/cdf-mech-sem\/tree\/master"},{"key":"1_CR26","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/S10817-008-9099-0, https:\/\/doi.org\/10.1007\/s10817-008-9099-0","DOI":"10.1007\/S10817-008-9099-0"},{"key":"1_CR27","unstructured":"Leroy, X., Blazy, S., K\u00e4stner, D., Schommer, B., Pister, M., Ferdinand, C.: CompCert - A Formally Verified Optimizing Compiler. In: ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress. SEE (Jan 2016)"},{"key":"1_CR28","doi-asserted-by":"publisher","unstructured":"Leroy, X., Grall, H.: Coinductive big-step operational semantics. Information and Computation 207(2), 284\u2013304 (2009). https:\/\/doi.org\/10.1016\/j.ic.2007.12.004","DOI":"10.1016\/j.ic.2007.12.004"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Mac\u00a0Carthy, J., Painter, J.: Correctness of a compiler for arithmetic expressions. Mathematical Aspects of Computer Science (1967)","DOI":"10.1090\/psapm\/019\/0242403"},{"key":"1_CR30","doi-asserted-by":"publisher","unstructured":"Mart\u00ednez, G., Ahman, D., Dumitrescu, V., Giannarakis, N., Hawblitzel, C., Hri\u0163cu, C., Narasimhamurthy, M., Paraskevopoulou, Z., Pit-Claudel, C., Protzenko, J., Ramananandro, T., Rastogi, A., Swamy, N.: Meta-F*: Proof automation with SMT, tactics, and metaprograms. In: Caires, L. (ed.) Programming Languages and Systems. pp. 30\u201359. Springer International Publishing, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17184-1_2, https:\/\/doi.org\/10.1007\/978-3-030-17184-1_2","DOI":"10.1007\/978-3-030-17184-1_2"},{"key":"1_CR31","unstructured":"Milner, R.J., Weyrauch, R.: Proving compiler correctness in a mechanized logic. Machine Intelligence 7, 51\u201373 (1972)"},{"key":"1_CR32","unstructured":"Pierce, Benjamin, e.a.: Software foundations - volume 1: logical foundations (2023), https:\/\/softwarefoundations.cis.upenn.edu\/lf-current\/Imp.html, version 6.6"},{"key":"1_CR33","doi-asserted-by":"publisher","unstructured":"Tassarotti, J., Tristan, J.B.: Verified density compilation for a probabilistic programming language. Proc. ACM Program. Lang. 7(PLDI) (jun 2023). https:\/\/doi.org\/10.1145\/3591245, https:\/\/doi.org\/10.1145\/3591245","DOI":"10.1145\/3591245"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57259-3_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T13:01:49Z","timestamp":1712322109000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57259-3_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572586","9783031572593"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57259-3_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"6 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/fase\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"14","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"34% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}