{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T19:18:55Z","timestamp":1781291935213,"version":"3.54.1"},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"7","license":[{"start":{"date-parts":[[2009,7,1]],"date-time":"2009-07-01T00:00:00Z","timestamp":1246406400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-05-SSIA-0019"],"award-info":[{"award-number":["ANR-05-SSIA-0019"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2009,7]]},"abstract":"<jats:p>This paper reports on the development and formal verification (proof of semantic preservation) of CompCert, a compiler from Clight (a large subset of the C programming language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a verified compiler is useful in the context of critical software and its formal verification: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.<\/jats:p>","DOI":"10.1145\/1538788.1538814","type":"journal-article","created":{"date-parts":[[2009,6,30]],"date-time":"2009-06-30T13:10:17Z","timestamp":1246367417000},"page":"107-115","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":911,"title":["Formal verification of a realistic compiler"],"prefix":"10.1145","volume":"52","author":[{"given":"Xavier","family":"Leroy","sequence":"first","affiliation":[{"name":"INRIA Paris-Rocquencourt, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2009,7]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/871816.871860"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792233.1792236"},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development---Coq'Art: The Calculus of Inductive Constructions","author":"Bertot Y.","year":"2004","unstructured":"]] Bertot , Y. , Cast\u00e9ran , P. Interactive Theorem Proving and Program Development---Coq'Art: The Calculus of Inductive Constructions ( 2004 ), Springer . ]]Bertot, Y., Cast\u00e9ran, P. Interactive Theorem Proving and Program Development---Coq'Art: The Calculus of Inductive Constructions (2004), Springer."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_31"},{"key":"e_1_2_1_5_1","volume-title":"Mechanized semantics for the Clight subset of the C language. J. Autom. Reasoning","author":"Blazy S.","year":"2009","unstructured":"]] Blazy , S. , Leroy , X. Mechanized semantics for the Clight subset of the C language. J. Autom. Reasoning ( 2009 ). Accepted for publication, to appear. ]]Blazy, S., Leroy, X. Mechanized semantics for the Clight subset of the C language. J. Autom. Reasoning (2009). Accepted for publication, to appear."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/800230.806984"},{"key":"e_1_2_1_7_1","volume-title":"The Coq proof assistant.","author":"Coq","year":"1989","unstructured":"]] Coq development team. The Coq proof assistant. Available at http:\/\/coq.inria.fr\/, 1989 --2009. ]]Coq development team. The Coq proof assistant. Available at http:\/\/coq.inria.fr\/, 1989--2009."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/966221.966235"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229546"},{"key":"e_1_2_1_10_1","first-page":"11","volume":"55","author":"Hales T.C.","year":"2008","unstructured":"]] Hales , T.C. Formal proof. Notices AMS 55 , 11 ( 2008 ), 1370--1380. ]]Hales, T.C. Formal proof. Notices AMS 55, 11 (2008), 1370--1380.","journal-title":"Notices AMS"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_1_12_1","unstructured":"]]Leroy X. The CompCert verified compiler software and commented proof. Available at http:\/\/compcert.inria.fr\/ Aug.2008.  ]]Leroy X. The CompCert verified compiler software and commented proof. Available at http:\/\/compcert.inria.fr\/ Aug.2008."},{"key":"e_1_2_1_13_1","volume-title":"July","author":"Leroy X.","year":"2008","unstructured":"]] Leroy , X. A formally verified compiler back-end. arXiv:0902.2137 {cs} . Submitted, July 2008 . ]]Leroy, X. A formally verified compiler back-end. arXiv:0902.2137 {cs}. Submitted, July 2008."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69407-6_39"},{"key":"e_1_2_1_16_1","series-title":"Proceedings of Symposia in Applied Mathematics (1967)","volume-title":"Mathematical Aspects of Computer Science","author":"McCarthy J.","unstructured":"]] McCarthy , J. , Painter , J. Correctness of a compiler for arithmetical expressions . In Mathematical Aspects of Computer Science , volume 19 of Proceedings of Symposia in Applied Mathematics (1967) , AMS , 33--41. ]]McCarthy, J., Painter, J. Correctness of a compiler for arithmetical expressions. In Mathematical Aspects of Computer Science, volume 19 of Proceedings of Symposia in Applied Mathematics (1967), AMS, 33--41."},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of 7th Annual Machine Intelligence Workshop","volume":"7","author":"Milner R.","year":"1972","unstructured":"]] Milner , R. , Weyhrauch , R. Proving compiler correctness in a mechanized logic . In Proceedings of 7th Annual Machine Intelligence Workshop , volume 7 of Machine Intelligence ( 1972 ), Edinburgh University Press, 51--72. ]]Milner, R., Weyhrauch, R. Proving compiler correctness in a mechanized logic. In Proceedings of 7th Annual Machine Intelligence Workshop, volume 7 of Machine Intelligence (1972), Edinburgh University Press, 51--72."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319345"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_2_1_21_1","series-title":"LNCS (2002)","volume-title":"Weimer","author":"Necula G.C.","unstructured":"]] Necula , G.C. , McPeak , S. , Rahul , S.P. , Weimer , W. CIL : Intermediate language and tools for analysis and transformation of C programs. In Compiler Construction, volume 2304 of LNCS (2002) , Springer , 213--228. ]]Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W. CIL: Intermediate language and tools for analysis and transformation of C programs. In Compiler Construction, volume 2304 of LNCS (2002), Springer, 213--228."},{"key":"e_1_2_1_22_1","series-title":"LNCS (1998)","volume-title":"Tools and Algorithms for Construction and Analysis of Systems, TACAS '98","author":"Pnueli A.","unstructured":"]] Pnueli , A. , Siegel , M. , Singerman , E. Translation validation . In Tools and Algorithms for Construction and Analysis of Systems, TACAS '98 , volume 1384 of LNCS (1998) , Springer , 151--166. ]]Pnueli, A., Siegel, M., Singerman, E. Translation validation. In Tools and Algorithms for Construction and Analysis of Systems, TACAS '98, volume 1384 of LNCS (1998), Springer, 151--166."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328444"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542512"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1538788.1538814","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1538788.1538814","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:38:47Z","timestamp":1750253927000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1538788.1538814"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,7]]},"references-count":24,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2009,7]]}},"alternative-id":["10.1145\/1538788.1538814"],"URL":"https:\/\/doi.org\/10.1145\/1538788.1538814","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,7]]},"assertion":[{"value":"2009-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}