{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:47:37Z","timestamp":1775868457191,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540372158","type":"print"},{"value":"9783540372165","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11813040_31","type":"book-chapter","created":{"date-parts":[[2006,8,7]],"date-time":"2006-08-07T10:51:03Z","timestamp":1154947863000},"page":"460-475","source":"Crossref","is-referenced-by-count":78,"title":["Formal Verification of a C Compiler Front-End"],"prefix":"10.1007","author":[{"given":"Sandrine","family":"Blazy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zaynah","family":"Dargaye","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xavier","family":"Leroy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"31_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/11576280_20","volume-title":"Formal Methods and Software Engineering","author":"S. Blazy","year":"2005","unstructured":"Blazy, S., Leroy, X.: Formal verification of a memory model for C-like imperative languages. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol.\u00a03785, pp. 280\u2013299. Springer, Heidelberg (2005)"},{"issue":"6","key":"31_CR2","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/966221.966235","volume":"28","author":"M.A. Dave","year":"2003","unstructured":"Dave, M.A.: Compiler verification: a bibliography. SIGSOFT Softw. Eng. Notes\u00a028(6), 2\u20132 (2003)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"issue":"2-3","key":"31_CR3","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/j.tcs.2004.11.008","volume":"336","author":"E. B\u00f6rger","year":"2005","unstructured":"B\u00f6rger, E., Fruja, N., Gervasi, V., St\u00e4rk, R.: A high-level modular definition of the semantics of C#. Theoretical Computer Science\u00a0336(2-3), 235\u2013284 (2005)","journal-title":"Theoretical Computer Science"},{"key":"31_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1007\/3-540-56992-8_17","volume-title":"Computer Science Logic","author":"Y. Gurevich","year":"1993","unstructured":"Gurevich, Y., Huggins, J.: The semantics of the C programming language. In: Martini, S., B\u00f6rger, E., Kleine B\u00fcning, H., J\u00e4ger, G., Richter, M.M. (eds.) CSL 1992. LNCS, vol.\u00a0702, pp. 274\u2013308. Springer, Heidelberg (1993)"},{"key":"31_CR5","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. Technical Report 0400001T.1, National ICT Australia, March 2004, in ACM TOPLAS (to appear) (2004)"},{"key":"31_CR6","first-page":"2","volume-title":"Proc. Conf. on Software Engineering and Formal Methods (SEFM)","author":"D. Leinenbach","year":"2005","unstructured":"Leinenbach, D., Paul, W., Petrova, E.: Towards the formal verification of a C0 compiler. In: Proc. Conf. on Software Engineering and Formal Methods (SEFM), Koblenz, Germany, September 2005, pp. 2\u201311. IEEE Computer Society Press, Los Alamitos (2005)"},{"key":"31_CR7","unstructured":"Leroy, X.: The Compcert certified compiler back-end \u2013 commented Coq development (2006), available online at: http:\/\/cristal.inria.fr\/~xleroy"},{"key":"31_CR8","first-page":"42","volume-title":"Proc. Symp. Principles Of Programming Languages (POPL)","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Proc. Symp. Principles Of Programming Languages (POPL), Charleston, USA, January 2006, pp. 42\u201354. ACM Press, New York (2006)"},{"key":"31_CR9","doi-asserted-by":"crossref","unstructured":"Nepomniaschy, V., Anureev, I., Promsky, A.: Verification-oriented language C-light and its structural operational semantics. In: Ershov Memorial Conference, pp. 103\u2013111 (2003)","DOI":"10.1007\/978-3-540-39866-0_12"},{"key":"31_CR10","unstructured":"Norrish, M.: C formalised in HOL. PhD thesis, University of Cambridge (December 1998)"},{"key":"31_CR11","unstructured":"Papaspyrou, N.: A formal semantics for the C programming language. PhD thesis, National Technical University of Athens (February 1998)"},{"key":"31_CR12","unstructured":"Strecker, M.: Compiler verification for C0. Technical report, Universit\u00e9 Paul Sabatier, Toulouse (April 2005)"}],"container-title":["Lecture Notes in Computer Science","FM 2006: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11813040_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:14:24Z","timestamp":1605644064000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11813040_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540372158","9783540372165"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/11813040_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}