{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T22:59:47Z","timestamp":1773097187469,"version":"3.50.1"},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2009,7,24]],"date-time":"2009-07-24T00:00:00Z","timestamp":1248393600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2009,10]]},"DOI":"10.1007\/s10817-009-9148-3","type":"journal-article","created":{"date-parts":[[2009,7,23]],"date-time":"2009-07-23T12:04:01Z","timestamp":1248350641000},"page":"263-288","source":"Crossref","is-referenced-by-count":133,"title":["Mechanized Semantics for the Clight Subset of the C Language"],"prefix":"10.1007","volume":"43","author":[{"given":"Sandrine","family":"Blazy","sequence":"first","affiliation":[]},{"given":"Xavier","family":"Leroy","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,7,24]]},"reference":[{"key":"9148_CR1","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1145\/1251535.1251543","volume-title":"PASTE \u201907: Proceedings of the 7th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering","author":"A Aiken","year":"2007","unstructured":"Aiken, A., Bugrara, S., Dillig, I., Dillig, T., Hackett, B., Hawkins, P.: An overview of the Saturn project. In: PASTE \u201907: Proceedings of the 7th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, pp. 43\u201348. ACM, New York (2007)"},{"key":"9148_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/978-3-540-74591-4_3","volume-title":"Theorem Proving in Higher Order Logics, 20th Int. Conf. TPHOLs 2007","author":"AW Appel","year":"2007","unstructured":"Appel, A.W., Blazy, S.: Separation logic for small-step Cminor. In: Theorem Proving in Higher Order Logics, 20th Int. Conf. TPHOLs 2007. Lecture Notes in Computer Science, vol. 4732, pp. 5\u201321. Springer, New York (2007)"},{"key":"9148_CR3","doi-asserted-by":"crossref","unstructured":"Appel, A.W., Leroy, X.: A list-machine benchmark for mechanized metatheory (extended abstract). In: Proc. Int. Workshop on Logical Frameworks and Meta-Languages (LFMTP\u201906). Electronic Notes in Computer Science, vol. 174\/5, pp. 95\u2013108 (2007)","DOI":"10.1016\/j.entcs.2007.01.020"},{"key":"9148_CR4","series-title":"EATCS Texts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development \u2013 Coq\u2019Art: the Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development \u2013 Coq\u2019Art: the Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science. Springer, New York (2004)"},{"key":"9148_CR5","first-page":"55","volume-title":"33rd Symposium on Principles of Programming Languages","author":"S Bishop","year":"2006","unstructured":"Bishop, S., Fairbairn, M., Norrish, M., Sewell, P., Smith, M., Wansbrough, K.: Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations. In: 33rd Symposium on Principles of Programming Languages, pp. 55\u201366. ACM, New York (2006)"},{"key":"9148_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"460","DOI":"10.1007\/11813040_31","volume-title":"FM 2006: 14th Int. Symp. on Formal Methods","author":"S Blazy","year":"2006","unstructured":"Blazy, S., Dargaye, Z., Leroy, X.: Formal verification of a C compiler front-end. In: FM 2006: 14th Int. Symp. on Formal Methods. Lecture Notes in Computer Science, vol. 4085, pp. 460\u2013475. Springer, New York (2006)"},{"issue":"2\u20133","key":"9148_CR7","doi-asserted-by":"crossref","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.F.: A high-level modular definition of the semantics of C#. Theor. Comp. Sci. 336(2\u20133), 235\u2013284 (2005)","journal-title":"Theor. Comp. Sci."},{"key":"9148_CR8","unstructured":"CEA LIST: FRAMA-C: framework for modular analysis of C. Software and documentation available on the web. http:\/\/frama-c.cea.fr\/ (2008)"},{"key":"9148_CR9","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1145\/781131.781157","volume-title":"PLDI \u201903: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation","author":"J Condit","year":"2003","unstructured":"Condit, J., Harren, M., McPeak, S., Necula, G.C., Weimer, W.: CCured in the real world. In: PLDI \u201903: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, pp. 232\u2013244. ACM, New York (2003)"},{"key":"9148_CR10","unstructured":"Coq Development Team: The Coq proof assistant. http:\/\/coq.inria.fr\/ (1989\u20132009)"},{"key":"9148_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/978-3-540-74591-4_7","volume-title":"Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007","author":"D Delahaye","year":"2007","unstructured":"Delahaye, D., Dubois, C., \u00c9tienne, J.F.: Extracting purely functional contents from logical inductive types. In: Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007. Lecture Notes in Computer Science, vol. 4732, pp. 70\u201385. Springer, New York (2007)"},{"key":"9148_CR12","unstructured":"Duff, T.: On Duff\u2019s device. http:\/\/www.lysator.liu.se\/c\/duffs-device.html . Message to the comp.lang.c Usenet Group (1988)"},{"key":"9148_CR13","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.C., March\u00e9, C.: Multi-prover verification of C programs. In: 6th Int. Conference on Formal Engineering Methods, ICFEM 2004. Lecture Notes in Computer Science, vol. 3308, pp. 15\u201329 (2004)","DOI":"10.1007\/978-3-540-30482-1_10"},{"key":"9148_CR14","unstructured":"Gimenez, E., Ledinot, E.: Semantics of a subset of the C language. Coq contributed library. http:\/\/coq.inria.fr\/contribs\/minic.html (2004)"},{"key":"9148_CR15","first-page":"235","volume-title":"International Conference on Functional Programming (ICFP 2002)","author":"B Gr\u00e9goire","year":"2002","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. In: International Conference on Functional Programming (ICFP 2002), pp. 235\u2013246. ACM, New York (2002)"},{"key":"9148_CR16","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, 6th Workshop, CSL \u201992","author":"Y Gurevich","year":"1993","unstructured":"Gurevich, Y., Huggins, J.: The semantics of the C programming language. In: Computer Science Logic, 6th Workshop, CSL \u201992. Lecture Notes in Computer Science, vol. 702, pp. 274\u2013308. Springer, New York (1993)"},{"issue":"6","key":"9148_CR17","doi-asserted-by":"crossref","first-page":"290","DOI":"10.1145\/1273442.1250767","volume":"42","author":"B Hardekopf","year":"2007","unstructured":"Hardekopf, B., Lin, C.: The ant and the grasshopper: fast and accurate pointer analysis for millions of lines of code. SIGPLAN Not. 42(6), 290\u2013299 (2007)","journal-title":"SIGPLAN Not."},{"issue":"4","key":"9148_CR18","doi-asserted-by":"crossref","first-page":"517","DOI":"10.1145\/503112.503115","volume":"33","author":"PH Hartel","year":"2001","unstructured":"Hartel, P.H., Moreau, L.: Formalizing the safety of Java, the Java virtual machine, and Java card. ACM Comput. Surv. 33(4), 517\u2013558 (2001)","journal-title":"ACM Comput. Surv."},{"issue":"7","key":"9148_CR19","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1016\/j.infsof.2003.09.016","volume":"46","author":"L Hatton","year":"2004","unstructured":"Hatton, L.: Safer language subsets: an overview and a case history, MISRA C. Inf. Soft. Technol. 46(7), 465\u2013472 (2004)","journal-title":"Inf. Soft. Technol."},{"key":"9148_CR20","doi-asserted-by":"crossref","unstructured":"Hoare, T., O\u2019Hearn, P.W.: Separation logic semantics for communicating processes. In: Proceedings of the First International Conference on Foundations of Informatics, Computing and Software (FICS 2008). Electronic Notes in Computer Science, vol. 212, pp. 3\u201325 (2008)","DOI":"10.1016\/j.entcs.2008.04.050"},{"key":"9148_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1007\/3-540-46428-X_20","volume-title":"Fundamental Approaches to Software Engineering, 3rd Int. Conf. FASE 2000","author":"M Huisman","year":"2000","unstructured":"Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Fundamental Approaches to Software Engineering, 3rd Int. Conf. FASE 2000. Lecture Notes in Computer Science, vol. 1783, pp. 284\u2013303. Springer, New York (2000)"},{"key":"9148_CR22","unstructured":"Hymans, C., Levillain, O.: Newspeak, doubleplussimple minilang for goodthinkful static analysis of C. Technical Note 2008-IW-SE-00010-1, EADS (2008)"},{"key":"9148_CR23","series-title":"Lecture Notes in Computer Science","first-page":"61","volume-title":"Higher Order Logic Theorem Proving and its Applications, 6th International Workshop, HUG \u201993","author":"M Inwegen van","year":"1993","unstructured":"van Inwegen, M., Gunter, E.L.: HOL-ML. In: Higher Order Logic Theorem Proving and its Applications, 6th International Workshop, HUG \u201993. Lecture Notes in Computer Science, vol. 780, pp. 61\u201374. Springer, New York (1993)"},{"issue":"4","key":"9148_CR24","doi-asserted-by":"crossref","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G Klein","year":"2006","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 (2006)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9148_CR25","first-page":"173","volume-title":"34th Symposium on Principles of Programming Languages","author":"DK Lee","year":"2007","unstructured":"Lee, D.K., Crary, K., Harper, R.: Towards a mechanized metatheory of Standard ML. In: 34th Symposium on Principles of Programming Languages, pp. 173\u2013184. ACM, New York (2007)"},{"key":"9148_CR26","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1109\/SEFM.2005.51","volume-title":"IEEE Conference on Software Engineering and Formal Methods (SEFM\u201905)","author":"D Leinenbach","year":"2005","unstructured":"Leinenbach, D., Paul, W., Petrova, E.: Towards the formal verification of a C0 compiler: code generation and implementation correctness. In: IEEE Conference on Software Engineering and Formal Methods (SEFM\u201905), pp. 2\u201311. IEEE Computer Society, Silver Spring (2005)"},{"key":"9148_CR27","first-page":"42","volume-title":"33rd ACM symposium on Principles of Programming Languages","author":"X Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd ACM symposium on Principles of Programming Languages, pp. 42\u201354. ACM, New York (2006)"},{"key":"9148_CR28","unstructured":"Leroy, X.: A formally verified compiler backend. arXiv:0902.2137 [cs] (2008)"},{"issue":"1","key":"9148_CR29","doi-asserted-by":"crossref","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."},{"issue":"2","key":"9148_CR30","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1016\/j.ic.2007.12.004","volume":"207","author":"X Leroy","year":"2007","unstructured":"Leroy, X., Grall, H.: Coinductive big-step operational semantics. Inf. Comput. 207(2), 284\u2013304 (2009). doi: 10.1016\/j.ic.2007.12.004","journal-title":"Inf. Comput."},{"key":"9148_CR31","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The Definition of Standard ML (Revised)","author":"R Milner","year":"1997","unstructured":"Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). MIT, Cambridge (1997)"},{"key":"9148_CR32","unstructured":"Motor Industry Software Reliability Association: MISRA-C. http:\/\/www.misra-c.com\/ (2004)"},{"key":"9148_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction, 11th International Conference, CC 2002","author":"GC Necula","year":"2002","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, 11th International Conference, CC 2002. Lecture Notes in Computer Science, vol. 2304, pp. 213\u2013228. Springer, New York (2002)"},{"issue":"6","key":"9148_CR34","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1023\/B:PACS.0000004134.24714.e5","volume":"29","author":"VA Nepomniaschy","year":"2003","unstructured":"Nepomniaschy, V.A., Anureev, I.S., Promsky, A.V.: Towards verification of C programs: axiomatic semantics of the C-kernel language. Program. Comput. Softw. 29(6), 338\u2013350 (2003)","journal-title":"Program. Comput. Softw."},{"key":"9148_CR35","volume-title":"Isabelle\/Hol: a Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2004","unstructured":"Nipkow, T., Paulson, L.C.: Isabelle\/Hol: a Proof Assistant for Higher-Order Logic. Springer, New York (2004)"},{"key":"9148_CR36","unstructured":"Norrish, M.: C formalised in HOL. Ph.D. thesis, University of Cambridge. Technical Report UCAM-CL-TR-453 (1998)"},{"key":"9148_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-49099-X_10","volume-title":"Programming Languages and Systems, 8th European Symposium on Programming, ESOP\u201999","author":"M Norrish","year":"1999","unstructured":"Norrish, M.: Deterministic expressions in C. In: Programming Languages and Systems, 8th European Symposium on Programming, ESOP\u201999. Lecture Notes in Computer Science, vol. 1576, pp. 147\u2013161. Springer, New York (1999)"},{"key":"9148_CR38","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Programming Languages and Systems, 17th European Symposium on Programming, ESOP 2008","author":"S Owens","year":"2008","unstructured":"Owens, S.: A sound semantics for OCamllight. In: Programming Languages and Systems, 17th European Symposium on Programming, ESOP 2008. Lecture Notes in Computer Science, vol. 4960, pp. 1\u201315. Springer, New York (2008)"},{"key":"9148_CR39","unstructured":"Papaspyrou, N.: A formal semantics for the C programming language. Ph.D. thesis, National Technical University of Athens (1998)"},{"key":"9148_CR40","unstructured":"Paul, W., et al.: The Verisoft project. http:\/\/www.verisoft.de\/ (2003\u20132008)"},{"key":"9148_CR41","doi-asserted-by":"crossref","unstructured":"Schirmer, N.: Verification of sequential imperative programs in Isabelle\/HOL. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2006)","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"9148_CR42","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1145\/1081706.1081750","volume-title":"ESEC\/FSE-13: Proceedings of the 10th European Software Engineering Conference","author":"K Sen","year":"2005","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: ESEC\/FSE-13: Proceedings of the 10th European Software Engineering Conference, pp. 263\u2013272. ACM, New York (2005)"},{"key":"9148_CR43","first-page":"1","volume-title":"Proceedings of the 12th International Conference on Functional Programming","author":"P Sewell","year":"2007","unstructured":"Sewell, P., Zappa Nardelli, F., Owens, S., Peskine, G., Ridge, T., Sarkar, S., Strnisa, R.: Ott: effective tool support for the working semanticist. In: Proceedings of the 12th International Conference on Functional Programming, pp. 1\u201312. ACM, New York (2007)"},{"key":"9148_CR44","unstructured":"Strecker, M.: Compiler verification for C0. Tech. Rep., Universit\u00e9 Paul Sabatier, Toulouse (2005)"},{"key":"9148_CR45","unstructured":"Tews, H.: Verifying Duff\u2019s device: a simple compositional denotational semantics for goto and computed jumps. http:\/\/www.cs.ru.nl\/~tews\/Goto\/goto.pdf . Draft Paper (2004)"},{"key":"9148_CR46","doi-asserted-by":"crossref","unstructured":"Tews, H., Weber, T., V\u00f6lp, M.: A formal model of memory peculiarities for the verification of low-level operating-system code. In: Proceedings of the International Workshop on Systems Software Verification (SSV\u201908). Electronic Notes in Computer Science, vol. 217, pp. 79\u201396 (2008)","DOI":"10.1016\/j.entcs.2008.06.043"},{"key":"9148_CR47","unstructured":"Tews, H., Weber, T., V\u00f6lp, M., Poll, E., van Eekelen, M., van Rossum, P.: Nova micro-hypervisor verification. Robin Project Deliverable D13, Radboud Universiteit Nijmegen. http:\/\/robin.tudos.org\/D.13 (2008)"},{"key":"9148_CR48","unstructured":"Zucker, S., Karhi, K.: System V application binary interface, PowerPC processor supplement. Tech. Rep. 802-3334-10, SunSoft (1995)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9148-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-009-9148-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9148-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:49Z","timestamp":1559265709000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-009-9148-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,7,24]]},"references-count":48,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,10]]}},"alternative-id":["9148"],"URL":"https:\/\/doi.org\/10.1007\/s10817-009-9148-3","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,7,24]]}}}